Theorem en2lp

Description: No class has 2-cycle membership loops. Theorem 7X(b) of Enderton p. 206. (Contributed by NM, 16-Oct-1996) (Revised by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Assertion	en2lp	⊢ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		zfregfr	⊢ E Fr V
2		efrn2lp	⊢ ( ( E Fr V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) )
3	1 2	mpan	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) )
4		elex	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
5		elex	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ V )
6	4 5	anim12i	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
7	6	con3i	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 ) )
8	3 7	pm2.61i	⊢ ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴 )