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

Metamath Proof Explorer

Theorem rspc4v

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

Ref Expression
Hypotheses rspc4v.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
rspc4v.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
rspc4v.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
rspc4v.4 ⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜓 ) )
Assertion rspc4v ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rspc4v.1 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
2 rspc4v.2 ⊢ ( 𝑦 = 𝐵 → ( 𝜒 ↔ 𝜃 ) )
3 rspc4v.3 ⊢ ( 𝑧 = 𝐶 → ( 𝜃 ↔ 𝜏 ) )
4 rspc4v.4 ⊢ ( 𝑤 = 𝐷 → ( 𝜏 ↔ 𝜓 ) )
5 df-3an ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) )
6 1 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑤 ∈ 𝑈 𝜑 ↔ ∀ 𝑤 ∈ 𝑈 𝜒 ) )
7 2 ralbidv ⊢ ( 𝑦 = 𝐵 → ( ∀ 𝑤 ∈ 𝑈 𝜒 ↔ ∀ 𝑤 ∈ 𝑈 𝜃 ) )
8 3 ralbidv ⊢ ( 𝑧 = 𝐶 → ( ∀ 𝑤 ∈ 𝑈 𝜃 ↔ ∀ 𝑤 ∈ 𝑈 𝜏 ) )
9 6 7 8 rspc3v ⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → ∀ 𝑤 ∈ 𝑈 𝜏 ) )
10 4 rspcv ⊢ ( 𝐷 ∈ 𝑈 → ( ∀ 𝑤 ∈ 𝑈 𝜏 → 𝜓 ) )
11 9 10 sylan9 ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ 𝐷 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )
12 5 11 sylanbr ⊢ ( ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ 𝐶 ∈ 𝑇 ) ∧ 𝐷 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )
13 12 anasss ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑇 ∀ 𝑤 ∈ 𝑈 𝜑 → 𝜓 ) )