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 ) = (/) ) )