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

Metamath Proof Explorer

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 A \to \neg A \in A$

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