Metamath Proof Explorer

Theorem scott0f

Description: A version of scott0 with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018)

Ref Expression
Hypotheses scott0f.1 ⊢Ⅎ_yA
scott0f.2 ⊢Ⅎ_xA
Assertion scott0f ⊢A=∅↔x∈A|∀y∈Arank⁡x⊆rank⁡y=∅

Proof

Step Hyp Ref Expression
1 scott0f.1 ⊢Ⅎ_yA
2 scott0f.2 ⊢Ⅎ_xA
3 scott0 ⊢A=∅↔w∈A|∀z∈Arank⁡w⊆rank⁡z=∅
4 nfcv ⊢Ⅎ_zA
5 nfv ⊢Ⅎzrank⁡x⊆rank⁡y
6 nfv ⊢Ⅎyrank⁡x⊆rank⁡z
7 fveq2 ⊢y=z→rank⁡y=rank⁡z
8 7 sseq2d ⊢y=z→rank⁡x⊆rank⁡y↔rank⁡x⊆rank⁡z
9 1 4 5 6 8 cbvralfw ⊢∀y∈Arank⁡x⊆rank⁡y↔∀z∈Arank⁡x⊆rank⁡z
10 9 rabbii ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y=x∈A|∀z∈Arank⁡x⊆rank⁡z
11 nfcv ⊢Ⅎ_wA
12 nfv ⊢Ⅎxrank⁡w⊆rank⁡z
13 2 12 nfralw ⊢Ⅎx∀z∈Arank⁡w⊆rank⁡z
14 nfv ⊢Ⅎw∀z∈Arank⁡x⊆rank⁡z
15 fveq2 ⊢w=x→rank⁡w=rank⁡x
16 15 sseq1d ⊢w=x→rank⁡w⊆rank⁡z↔rank⁡x⊆rank⁡z
17 16 ralbidv ⊢w=x→∀z∈Arank⁡w⊆rank⁡z↔∀z∈Arank⁡x⊆rank⁡z
18 11 2 13 14 17 cbvrabw ⊢w∈A|∀z∈Arank⁡w⊆rank⁡z=x∈A|∀z∈Arank⁡x⊆rank⁡z
19 10 18 eqtr4i ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y=w∈A|∀z∈Arank⁡w⊆rank⁡z
20 19 eqeq1i ⊢x∈A|∀y∈Arank⁡x⊆rank⁡y=∅↔w∈A|∀z∈Arank⁡w⊆rank⁡z=∅
21 3 20 bitr4i ⊢A=∅↔x∈A|∀y∈Arank⁡x⊆rank⁡y=∅