Metamath Proof Explorer

Theorem scottexs

Description: Theorem scheme version of scottex . The collection of all x of minimum rank such that ph ( x ) is true, is a set. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scottexs ⊢x|φ∧∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y∈V

Proof

Step Hyp Ref Expression
1 nfcv ⊢Ⅎ_zx|φ
2 nfab1 ⊢Ⅎ_xx|φ
3 nfv ⊢Ⅎxrank⁡z⊆rank⁡y
4 2 3 nfralw ⊢Ⅎx∀y∈x|φrank⁡z⊆rank⁡y
5 nfv ⊢Ⅎz∀y∈x|φrank⁡x⊆rank⁡y
6 fveq2 ⊢z=x→rank⁡z=rank⁡x
7 6 sseq1d ⊢z=x→rank⁡z⊆rank⁡y↔rank⁡x⊆rank⁡y
8 7 ralbidv ⊢z=x→∀y∈x|φrank⁡z⊆rank⁡y↔∀y∈x|φrank⁡x⊆rank⁡y
9 1 2 4 5 8 cbvrabw ⊢z∈x|φ|∀y∈x|φrank⁡z⊆rank⁡y=x∈x|φ|∀y∈x|φrank⁡x⊆rank⁡y
10 df-rab ⊢x∈x|φ|∀y∈x|φrank⁡x⊆rank⁡y=x|x∈x|φ∧∀y∈x|φrank⁡x⊆rank⁡y
11 abid ⊢x∈x|φ↔φ
12 df-ral ⊢∀y∈x|φrank⁡x⊆rank⁡y↔∀yy∈x|φ→rank⁡x⊆rank⁡y
13 df-sbc ⊢[˙y/x]˙φ↔y∈x|φ
14 13 imbi1i ⊢[˙y/x]˙φ→rank⁡x⊆rank⁡y↔y∈x|φ→rank⁡x⊆rank⁡y
15 14 albii ⊢∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y↔∀yy∈x|φ→rank⁡x⊆rank⁡y
16 12 15 bitr4i ⊢∀y∈x|φrank⁡x⊆rank⁡y↔∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y
17 11 16 anbi12i ⊢x∈x|φ∧∀y∈x|φrank⁡x⊆rank⁡y↔φ∧∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y
18 17 abbii ⊢x|x∈x|φ∧∀y∈x|φrank⁡x⊆rank⁡y=x|φ∧∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y
19 9 10 18 3eqtri ⊢z∈x|φ|∀y∈x|φrank⁡z⊆rank⁡y=x|φ∧∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y
20 scottex ⊢z∈x|φ|∀y∈x|φrank⁡z⊆rank⁡y∈V
21 19 20 eqeltrri ⊢x|φ∧∀y[˙y/x]˙φ→rank⁡x⊆rank⁡y∈V