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	$$⊢\neg \left(A\in B\wedge B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		zfregfr	$$⊢\mathrm{E}\mathrm{Fr}\mathrm{V}$$
2		efrn2lp	$$⊢\left(\mathrm{E}\mathrm{Fr}\mathrm{V}\wedge \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\right)\to \neg \left(A\in B\wedge B\in A\right)$$
3	1 2	mpan	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \neg \left(A\in B\wedge B\in A\right)$$
4		elex	$$⊢A\in B\to A\in \mathrm{V}$$
5		elex	$$⊢B\in A\to B\in \mathrm{V}$$
6	4 5	anim12i	$$⊢\left(A\in B\wedge B\in A\right)\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
7	6	con3i	$$⊢\neg \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \neg \left(A\in B\wedge B\in A\right)$$
8	3 7	pm2.61i	$$⊢\neg \left(A\in B\wedge B\in A\right)$$