Theorem efrirr

Description: A well-founded class does not belong to itself. (Contributed by NM, 18-Apr-1994) (Revised by Mario Carneiro, 22-Jun-2015)

	Ref	Expression
Assertion	efrirr	$$⊢\mathrm{E}\mathrm{Fr}A\to \neg A\in A$$

Proof

Step	Hyp	Ref	Expression
1		frirr	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge A\in A\right)\to \neg A\mathrm{E}A$$
2		epelg	$$⊢A\in A\to \left(A\mathrm{E}A\leftrightarrow A\in A\right)$$
3	2	adantl	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge A\in A\right)\to \left(A\mathrm{E}A\leftrightarrow A\in A\right)$$
4	1 3	mtbid	$$⊢\left(\mathrm{E}\mathrm{Fr}A\wedge A\in A\right)\to \neg A\in A$$
5	4	pm2.01da	$$⊢\mathrm{E}\mathrm{Fr}A\to \neg A\in A$$