Theorem rspc6v

Description: 6-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 20-Feb-2025)

	Ref	Expression
Hypotheses	rspc6v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	rspc6v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
	rspc6v.3	⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
	rspc6v.4	⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜂 ) )
	rspc6v.5	⊢ ( 𝑝 = 𝐸 → ( 𝜂 ↔ 𝜁 ) )
	rspc6v.6	⊢ ( 𝑞 = 𝐹 → ( 𝜁 ↔ 𝜓 ) )
Assertion	rspc6v	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rspc6v.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2		rspc6v.2	⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3		rspc6v.3	⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
4		rspc6v.4	⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜂 ) )
5		rspc6v.5	⊢ ( 𝑝 = 𝐸 → ( 𝜂 ↔ 𝜁 ) )
6		rspc6v.6	⊢ ( 𝑞 = 𝐹 → ( 𝜁 ↔ 𝜓 ) )
7	1	2ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜑 ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜒 ) )
8	2	2ralbidv	⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜒 ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜃 ) )
9	3	2ralbidv	⊢ ( 𝑧 = 𝐶 → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜃 ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜏 ) )
10	4	2ralbidv	⊢ ( 𝑤 = 𝐷 → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜏 ↔ ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜂 ) )
11	7 8 9 10	rspc4v	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜑 → ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜂 ) )
12	5 6	rspc2v	⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜂 → 𝜓 ) )
13	11 12	syl9	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜑 → 𝜓 ) ) )
14	13	3impia	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ∧ ( 𝐸 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 ∀ 𝑝 ∈ 𝑉 ∀ 𝑞 ∈ 𝑊 𝜑 → 𝜓 ) )