This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Founded and well-ordering relations dffr2ALT
Description: Alternate proof of dffr2 , which avoids ax-8 but requires ax-10 ,
ax-11 , ax-12 . (Contributed by NM , 17-Feb-2004) (Proof shortened by Andrew Salmon , 27-Aug-2011) (Proof shortened by Mario Carneiro , 23-Jun-2015) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Assertion
dffr2ALT |- ( 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 } = (/) ) )