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

Metamath Proof Explorer

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 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 𝜓 )