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

Metamath Proof Explorer

Theorem dfepfr

Description: An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004) (Revised by Mario Carneiro, 23-Jun-2015)

Ref Expression
Assertion dfepfr 
|- ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 dffr2 
 |-  ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) )
2 epel 
 |-  ( z _E y <-> z e. y )
3 2 rabbii 
 |-  { z e. x | z _E y } = { z e. x | z e. y }
4 dfin5 
 |-  ( x i^i y ) = { z e. x | z e. y }
5 3 4 eqtr4i 
 |-  { z e. x | z _E y } = ( x i^i y )
6 5 eqeq1i 
 |-  ( { z e. x | z _E y } = (/) <-> ( x i^i y ) = (/) )
7 6 rexbii 
 |-  ( E. y e. x { z e. x | z _E y } = (/) <-> E. y e. x ( x i^i y ) = (/) )
8 7 imbi2i 
 |-  ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )
9 8 albii 
 |-  ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z _E y } = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )
10 1 9 bitri 
 |-  ( _E Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i y ) = (/) ) )