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	⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		frirr	⊢ ( ( E Fr 𝐴 ∧ 𝐴 ∈ 𝐴 ) → ¬ 𝐴 E 𝐴 )
2		epelg	⊢ ( 𝐴 ∈ 𝐴 → ( 𝐴 E 𝐴 ↔ 𝐴 ∈ 𝐴 ) )
3	2	adantl	⊢ ( ( E Fr 𝐴 ∧ 𝐴 ∈ 𝐴 ) → ( 𝐴 E 𝐴 ↔ 𝐴 ∈ 𝐴 ) )
4	1 3	mtbid	⊢ ( ( E Fr 𝐴 ∧ 𝐴 ∈ 𝐴 ) → ¬ 𝐴 ∈ 𝐴 )
5	4	pm2.01da	⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴 )