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

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 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion rspc2gv ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rspc2gv.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝑊 𝜑 ) )
3 df-ral ⊢ ( ∀ 𝑦 ∈ 𝑊 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) )
4 3 imbi2i ⊢ ( ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝑊 𝜑 ) ↔ ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
5 4 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝑊 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
6 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) ↔ ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
7 6 bicomi ⊢ ( ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
8 7 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
9 impexp ⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) → 𝜑 ) ↔ ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) )
10 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉 ) )
11 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
12 10 11 bi2anan9 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ↔ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) )
13 12 1 imbi12d ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜓 ) ) )
14 9 13 bitr3id ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) ↔ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜓 ) ) )
15 14 spc2gv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝜓 ) ) )
16 15 pm2.43a ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ∈ 𝑉 → ( 𝑦 ∈ 𝑊 → 𝜑 ) ) → 𝜓 ) )
17 8 16 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) → 𝜓 ) )
18 5 17 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝑊 𝜑 ) → 𝜓 ) )
19 2 18 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜑 → 𝜓 ) )