Metamath Proof Explorer

Theorem rspc2gv

Description: Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021)

Ref Expression
Hypothesis rspc2gv.1 ⊢ x = A ∧ y = B → φ ↔ ψ
Assertion rspc2gv ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ V ∀ y ∈ W φ → ψ

Proof

Step Hyp Ref Expression
1 rspc2gv.1 ⊢ x = A ∧ y = B → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ V ∀ y ∈ W φ ↔ ∀ x x ∈ V → ∀ y ∈ W φ
3 df-ral ⊢ ∀ y ∈ W φ ↔ ∀ y y ∈ W → φ
4 3 imbi2i ⊢ x ∈ V → ∀ y ∈ W φ ↔ x ∈ V → ∀ y y ∈ W → φ
5 4 albii ⊢ ∀ x x ∈ V → ∀ y ∈ W φ ↔ ∀ x x ∈ V → ∀ y y ∈ W → φ
6 19.21v ⊢ ∀ y x ∈ V → y ∈ W → φ ↔ x ∈ V → ∀ y y ∈ W → φ
7 6 bicomi ⊢ x ∈ V → ∀ y y ∈ W → φ ↔ ∀ y x ∈ V → y ∈ W → φ
8 7 albii ⊢ ∀ x x ∈ V → ∀ y y ∈ W → φ ↔ ∀ x ∀ y x ∈ V → y ∈ W → φ
9 impexp ⊢ x ∈ V ∧ y ∈ W → φ ↔ x ∈ V → y ∈ W → φ
10 eleq1 ⊢ x = A → x ∈ V ↔ A ∈ V
11 eleq1 ⊢ y = B → y ∈ W ↔ B ∈ W
12 10 11 bi2anan9 ⊢ x = A ∧ y = B → x ∈ V ∧ y ∈ W ↔ A ∈ V ∧ B ∈ W
13 12 1 imbi12d ⊢ x = A ∧ y = B → x ∈ V ∧ y ∈ W → φ ↔ A ∈ V ∧ B ∈ W → ψ
14 9 13 bitr3id ⊢ x = A ∧ y = B → x ∈ V → y ∈ W → φ ↔ A ∈ V ∧ B ∈ W → ψ
15 14 spc2gv ⊢ A ∈ V ∧ B ∈ W → ∀ x ∀ y x ∈ V → y ∈ W → φ → A ∈ V ∧ B ∈ W → ψ
16 15 pm2.43a ⊢ A ∈ V ∧ B ∈ W → ∀ x ∀ y x ∈ V → y ∈ W → φ → ψ
17 8 16 syl5bi ⊢ A ∈ V ∧ B ∈ W → ∀ x x ∈ V → ∀ y y ∈ W → φ → ψ
18 5 17 syl5bi ⊢ A ∈ V ∧ B ∈ W → ∀ x x ∈ V → ∀ y ∈ W φ → ψ
19 2 18 syl5bi ⊢ A ∈ V ∧ B ∈ W → ∀ x ∈ V ∀ y ∈ W φ → ψ