This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ B ∧ B ∈ A

Proof

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