Theorem dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	dffr4	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		dffr3	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
2		df-pred	|- Pred ( R , x , y ) = ( x i^i ( `' R " { y } ) )
3	2	eqeq1i	|- ( Pred ( R , x , y ) = (/) <-> ( x i^i ( `' R " { y } ) ) = (/) )
4	3	rexbii	|- ( E. y e. x Pred ( R , x , y ) = (/) <-> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) )
5	4	imbi2i	|- ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
6	5	albii	|- ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
7	1 6	bitr4i	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) )