This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffr6

Description: Alternate definition of df-fr . See dffr5 for a definition without dummy variables (but note that their equivalence uses ax-sep ). (Contributed by BJ, 16-Nov-2024)

Ref Expression
Assertion dffr6 
|- ( R Fr A <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )

Proof

Step Hyp Ref Expression
1 velpw 
 |-  ( x e. ~P A <-> x C_ A )
2 1 bicomi 
 |-  ( x C_ A <-> x e. ~P A )
3 velsn 
 |-  ( x e. { (/) } <-> x = (/) )
4 3 bicomi 
 |-  ( x = (/) <-> x e. { (/) } )
5 4 necon3abii 
 |-  ( x =/= (/) <-> -. x e. { (/) } )
6 2 5 anbi12i 
 |-  ( ( x C_ A /\ x =/= (/) ) <-> ( x e. ~P A /\ -. x e. { (/) } ) )
7 eldif 
 |-  ( x e. ( ~P A \ { (/) } ) <-> ( x e. ~P A /\ -. x e. { (/) } ) )
8 6 7 bitr4i 
 |-  ( ( x C_ A /\ x =/= (/) ) <-> x e. ( ~P A \ { (/) } ) )
9 8 imbi1i 
 |-  ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> ( x e. ( ~P A \ { (/) } ) -> E. y e. x A. z e. x -. z R y ) )
10 9 albii 
 |-  ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> A. x ( x e. ( ~P A \ { (/) } ) -> E. y e. x A. z e. x -. z R y ) )
11 df-fr 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
12 df-ral 
 |-  ( A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y <-> A. x ( x e. ( ~P A \ { (/) } ) -> E. y e. x A. z e. x -. z R y ) )
13 10 11 12 3bitr4i 
 |-  ( R Fr A <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )