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

Metamath Proof Explorer

Theorem cbvral2vw

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

Ref Expression
Hypotheses cbvral2vw.1 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜒 ) )
cbvral2vw.2 ⊢ ( 𝑦 = 𝑤 → ( 𝜒 ↔ 𝜓 ) )
Assertion cbvral2vw ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐵 𝜓 )

Proof

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