Metamath Proof Explorer


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