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 ⊢RFrA↔∀x∈𝒫A∖∅∃y∈x∀z∈x¬zRy

Proof

Step Hyp Ref Expression
1 velpw ⊢x∈𝒫A↔x⊆A
2 1 bicomi ⊢x⊆A↔x∈𝒫A
3 velsn ⊢x∈∅↔x=∅
4 3 bicomi ⊢x=∅↔x∈∅
5 4 necon3abii ⊢x≠∅↔¬x∈∅
6 2 5 anbi12i ⊢x⊆A∧x≠∅↔x∈𝒫A∧¬x∈∅
7 eldif ⊢x∈𝒫A∖∅↔x∈𝒫A∧¬x∈∅
8 6 7 bitr4i ⊢x⊆A∧x≠∅↔x∈𝒫A∖∅
9 8 imbi1i ⊢x⊆A∧x≠∅→∃y∈x∀z∈x¬zRy↔x∈𝒫A∖∅→∃y∈x∀z∈x¬zRy
10 9 albii ⊢∀xx⊆A∧x≠∅→∃y∈x∀z∈x¬zRy↔∀xx∈𝒫A∖∅→∃y∈x∀z∈x¬zRy
11 df-fr ⊢RFrA↔∀xx⊆A∧x≠∅→∃y∈x∀z∈x¬zRy
12 df-ral ⊢∀x∈𝒫A∖∅∃y∈x∀z∈x¬zRy↔∀xx∈𝒫A∖∅→∃y∈x∀z∈x¬zRy
13 10 11 12 3bitr4i ⊢RFrA↔∀x∈𝒫A∖∅∃y∈x∀z∈x¬zRy