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

Metamath Proof Explorer

Theorem vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019) (Proof shortened by Wolf Lammen, 31-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		vtocl4ga.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		vtocl4ga.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3		vtocl4ga.3	⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜌 ) )
4		vtocl4ga.4	⊢ ( 𝑤 = 𝐷 → ( 𝜌 ↔ 𝜃 ) )
5		vtocl4ga.5	⊢ ( ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) ∧ ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) ) → 𝜑 )
6	3	imbi2d	⊢ ( 𝑧 = 𝐶 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜌 ) ) )
7	4	imbi2d	⊢ ( 𝑤 = 𝐷 → ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜌 ) ↔ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) ) )
8	1	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜑 ) ↔ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜓 ) ) )
9	2	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜓 ) ↔ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜒 ) ) )
10	5	ex	⊢ ( ( 𝑥 ∈ 𝑄 ∧ 𝑦 ∈ 𝑅 ) → ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜑 ) )
11	8 9 10	vtocl2ga	⊢ ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → 𝜒 ) )
12	11	com12	⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑇 ) → ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 ) )
13	6 7 12	vtocl2ga	⊢ ( ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) → ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) )
14	13	impcom	⊢ ( ( ( 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑅 ) ∧ ( 𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑇 ) ) → 𝜃 )