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
|- -. ( A e. B /\ B e. A )

Proof

Step Hyp Ref Expression
1 zfregfr
 |-  _E Fr _V
2 efrn2lp
 |-  ( ( _E Fr _V /\ ( A e. _V /\ B e. _V ) ) -> -. ( A e. B /\ B e. A ) )
3 1 2 mpan
 |-  ( ( A e. _V /\ B e. _V ) -> -. ( A e. B /\ B e. A ) )
4 elex
 |-  ( A e. B -> A e. _V )
5 elex
 |-  ( B e. A -> B e. _V )
6 4 5 anim12i
 |-  ( ( A e. B /\ B e. A ) -> ( A e. _V /\ B e. _V ) )
7 6 con3i
 |-  ( -. ( A e. _V /\ B e. _V ) -> -. ( A e. B /\ B e. A ) )
8 3 7 pm2.61i
 |-  -. ( A e. B /\ B e. A )