Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Assertion	dffr2	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fr	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
2		rabeq0	|- ( { z e. x | z R y } = (/) <-> A. z e. x -. z R y )
3	2	rexbii	|- ( E. y e. x { z e. x | z R y } = (/) <-> E. y e. x A. z e. x -. z R y )
4	3	imbi2i	|- ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
5	4	albii	|- ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
6	1 5	bitr4i	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )