ax-baihei-inj - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-baihei-inj

Axiom ax-baihei-inj 473

Description: The successor function is injective. A standard axiom of second-order arithmetic.

**Assertion**
Ref	Expression
ax-baihei-inj	⊢ ganai li 1+ ku'i'a du li 1+ ku'i'e gi li ku'i'a du li ku'i'e

Distinct variable group: ku'i'a ,ku'i'e

This axiom is referenced by: baihei-inj 474