ax-baihei-inj - brismu bridi

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

Axiom ax-baihei-inj 577

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

**Assertion**
Ref	Expression
ax-baihei-inj	⊢ ganai li bai'ei ku'i'a du li bai'ei 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 578