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 ⊢ Ⅎ _ z x | φ
2 nfab1 ⊢ Ⅎ _ x x | φ
3 nfv ⊢ Ⅎ x rank ⁡ 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 ↔ ∀ y y ∈ 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 ↔ ∀ y y ∈ 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