Metamath Proof Explorer


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 ¬ ( 𝐴𝐵𝐵𝐴 )