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