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 )