Theorem ordirr

Description: No ordinal class is a member of itself. In other words, the membership relation is irreflexive on ordinal classes. Theorem 2.2(i) of BellMachover p. 469, generalized to classes. We prove this without invoking the Axiom of Regularity. (Contributed by NM, 2-Jan-1994)

	Ref	Expression
Assertion	ordirr	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordfr	⊢ ( Ord 𝐴 → E Fr 𝐴 )
2		efrirr	⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴 )
3	1 2	syl	⊢ ( Ord 𝐴 → ¬ 𝐴 ∈ 𝐴 )