Theorem elirrv

Description: The membership relation is irreflexive: no set is a member of itself. Theorem 105 of Suppes p. 54. (This is trivial to prove from zfregfr and efrirr , but this proof is direct from the Axiom of Regularity.) (Contributed by NM, 19-Aug-1993)

	Ref	Expression
Assertion	elirrv	⊢ ¬ 𝑥 ∈ 𝑥

Proof

Step	Hyp	Ref	Expression
1		snex	⊢ { 𝑥 } ∈ V
2		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 } ↔ 𝑥 ∈ { 𝑥 } ) )
3		vsnid	⊢ 𝑥 ∈ { 𝑥 }
4	2 3	speivw	⊢ ∃ 𝑦 𝑦 ∈ { 𝑥 }
5		zfregcl	⊢ ( { 𝑥 } ∈ V → ( ∃ 𝑦 𝑦 ∈ { 𝑥 } → ∃ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } ) )
6	1 4 5	mp2	⊢ ∃ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 }
7		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
8		ax9	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
9	8	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝑥 → 𝑥 ∈ 𝑦 ) )
10	9	com12	⊢ ( 𝑥 ∈ 𝑥 → ( 𝑦 = 𝑥 → 𝑥 ∈ 𝑦 ) )
11	7 10	syl5bi	⊢ ( 𝑥 ∈ 𝑥 → ( 𝑦 ∈ { 𝑥 } → 𝑥 ∈ 𝑦 ) )
12		eleq1w	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∈ { 𝑥 } ↔ 𝑥 ∈ { 𝑥 } ) )
13	12	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ∈ { 𝑥 } ↔ ¬ 𝑥 ∈ { 𝑥 } ) )
14	13	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } → ( 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ { 𝑥 } ) )
15	3 14	mt2i	⊢ ( ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } → ¬ 𝑥 ∈ 𝑦 )
16	11 15	nsyli	⊢ ( 𝑥 ∈ 𝑥 → ( ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } → ¬ 𝑦 ∈ { 𝑥 } ) )
17	16	con2d	⊢ ( 𝑥 ∈ 𝑥 → ( 𝑦 ∈ { 𝑥 } → ¬ ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } ) )
18	17	ralrimiv	⊢ ( 𝑥 ∈ 𝑥 → ∀ 𝑦 ∈ { 𝑥 } ¬ ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } )
19		ralnex	⊢ ( ∀ 𝑦 ∈ { 𝑥 } ¬ ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } ↔ ¬ ∃ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } )
20	18 19	sylib	⊢ ( 𝑥 ∈ 𝑥 → ¬ ∃ 𝑦 ∈ { 𝑥 } ∀ 𝑧 ∈ 𝑦 ¬ 𝑧 ∈ { 𝑥 } )
21	6 20	mt2	⊢ ¬ 𝑥 ∈ 𝑥