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	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ( 𝑦 ∈ 𝑊 → 𝜑 ) ) → 𝜓 ) )
18	5 17	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ( 𝑥 ∈ 𝑉 → ∀ 𝑦 ∈ 𝑊 𝜑 ) → 𝜓 ) )
19	2 18	syl5bi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑊 𝜑 → 𝜓 ) )