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

Metamath Proof Explorer

Theorem cbvral6vw

Description: Change bound variables of sextuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 5-Mar-2025)

		Ref	Expression
	Hypotheses	cbvral6vw.1	⊢ ( 𝑥 = 𝑎 → ( 𝜑 ↔ 𝜒 ) )
		cbvral6vw.2	⊢ ( 𝑦 = 𝑏 → ( 𝜒 ↔ 𝜃 ) )
		cbvral6vw.3	⊢ ( 𝑧 = 𝑐 → ( 𝜃 ↔ 𝜏 ) )
		cbvral6vw.4	⊢ ( 𝑤 = 𝑑 → ( 𝜏 ↔ 𝜂 ) )
		cbvral6vw.5	⊢ ( 𝑝 = 𝑒 → ( 𝜂 ↔ 𝜁 ) )
		cbvral6vw.6	⊢ ( 𝑞 = 𝑓 → ( 𝜁 ↔ 𝜓 ) )
	Assertion	cbvral6vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐷 ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜑 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ 𝐷 ∀ 𝑒 ∈ 𝐸 ∀ 𝑓 ∈ 𝐹 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvral6vw.1	⊢ ( 𝑥 = 𝑎 → ( 𝜑 ↔ 𝜒 ) )
2		cbvral6vw.2	⊢ ( 𝑦 = 𝑏 → ( 𝜒 ↔ 𝜃 ) )
3		cbvral6vw.3	⊢ ( 𝑧 = 𝑐 → ( 𝜃 ↔ 𝜏 ) )
4		cbvral6vw.4	⊢ ( 𝑤 = 𝑑 → ( 𝜏 ↔ 𝜂 ) )
5		cbvral6vw.5	⊢ ( 𝑝 = 𝑒 → ( 𝜂 ↔ 𝜁 ) )
6		cbvral6vw.6	⊢ ( 𝑞 = 𝑓 → ( 𝜁 ↔ 𝜓 ) )
7	1	2ralbidv	⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜑 ↔ ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜒 ) )
8	2	2ralbidv	⊢ ( 𝑦 = 𝑏 → ( ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜒 ↔ ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜃 ) )
9	3	2ralbidv	⊢ ( 𝑧 = 𝑐 → ( ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜃 ↔ ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜏 ) )
10	4	2ralbidv	⊢ ( 𝑤 = 𝑑 → ( ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜏 ↔ ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜂 ) )
11	7 8 9 10	cbvral4vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐷 ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜑 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ 𝐷 ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜂 )
12	5 6	cbvral2vw	⊢ ( ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜂 ↔ ∀ 𝑒 ∈ 𝐸 ∀ 𝑓 ∈ 𝐹 𝜓 )
13	12	4ralbii	⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ 𝐷 ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜂 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ 𝐷 ∀ 𝑒 ∈ 𝐸 ∀ 𝑓 ∈ 𝐹 𝜓 )
14	11 13	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 ∀ 𝑤 ∈ 𝐷 ∀ 𝑝 ∈ 𝐸 ∀ 𝑞 ∈ 𝐹 𝜑 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ 𝐷 ∀ 𝑒 ∈ 𝐸 ∀ 𝑓 ∈ 𝐹 𝜓 )