Theorem cbvral3vw

Description: Change bound variables of triple restricted universal quantification, using implicit substitution. Version of cbvral3v with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-May-2005) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

	Ref	Expression
Hypotheses	cbvral3vw.1	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
	cbvral3vw.2	⊢ ( 𝑦 = 𝑣 → ( 𝜒 ↔ 𝜃 ) )
	cbvral3vw.3	⊢ ( 𝑧 = 𝑢 → ( 𝜃 ↔ 𝜓 ) )
Assertion	cbvral3vw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvral3vw.1	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜒 ) )
2		cbvral3vw.2	⊢ ( 𝑦 = 𝑣 → ( 𝜒 ↔ 𝜃 ) )
3		cbvral3vw.3	⊢ ( 𝑧 = 𝑢 → ( 𝜃 ↔ 𝜓 ) )
4	1	2ralbidv	⊢ ( 𝑥 = 𝑤 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ) )
5	4	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 )
6	2 3	cbvral2vw	⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ↔ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 )
7	6	ralbii	⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜒 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 )
8	5 7	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 )