This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspc2vd

Description: Deduction version of 2-variable restricted specialization, using implicit substitution. Notice that the class D for the second set variable y may depend on the first set variable x . (Contributed by AV, 29-Mar-2021)

Ref Expression
Hypotheses rspc2vd.a ⊢ x = A → θ ↔ χ
rspc2vd.b ⊢ y = B → χ ↔ ψ
rspc2vd.c ⊢ φ → A ∈ C
rspc2vd.d ⊢ φ ∧ x = A → D = E
rspc2vd.e ⊢ φ → B ∈ E
Assertion rspc2vd ⊢ φ → ∀ x ∈ C ∀ y ∈ D θ → ψ

Proof

Step Hyp Ref Expression
1 rspc2vd.a ⊢ x = A → θ ↔ χ
2 rspc2vd.b ⊢ y = B → χ ↔ ψ
3 rspc2vd.c ⊢ φ → A ∈ C
4 rspc2vd.d ⊢ φ ∧ x = A → D = E
5 rspc2vd.e ⊢ φ → B ∈ E
6 3 4 csbied ⊢ φ → ⦋ A / x⦌ D = E
7 5 6 eleqtrrd ⊢ φ → B ∈ ⦋ A / x⦌ D
8 nfcsb1v ⊢ Ⅎ _ x ⦋ A / x⦌ D
9 nfv ⊢ Ⅎ x χ
10 8 9 nfralw ⊢ Ⅎ x ∀ y ∈ ⦋ A / x⦌ D χ
11 csbeq1a ⊢ x = A → D = ⦋ A / x⦌ D
12 11 1 raleqbidv ⊢ x = A → ∀ y ∈ D θ ↔ ∀ y ∈ ⦋ A / x⦌ D χ
13 10 12 rspc ⊢ A ∈ C → ∀ x ∈ C ∀ y ∈ D θ → ∀ y ∈ ⦋ A / x⦌ D χ
14 3 13 syl ⊢ φ → ∀ x ∈ C ∀ y ∈ D θ → ∀ y ∈ ⦋ A / x⦌ D χ
15 2 rspcv ⊢ B ∈ ⦋ A / x⦌ D → ∀ y ∈ ⦋ A / x⦌ D χ → ψ
16 7 14 15 sylsyld ⊢ φ → ∀ x ∈ C ∀ y ∈ D θ → ψ