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 -> -. A e. A )

Proof

Step Hyp Ref Expression
1 frirr 
 |-  ( ( _E Fr A /\ A e. A ) -> -. A _E A )
2 epelg 
 |-  ( A e. A -> ( A _E A <-> A e. A ) )
3 2 adantl 
 |-  ( ( _E Fr A /\ A e. A ) -> ( A _E A <-> A e. A ) )
4 1 3 mtbid 
 |-  ( ( _E Fr A /\ A e. A ) -> -. A e. A )
5 4 pm2.01da 
 |-  ( _E Fr A -> -. A e. A )