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 Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvral2vw.1 ⊢x=z→φ↔χ
cbvral2vw.2 ⊢y=w→χ↔ψ
Assertion cbvral2vw ⊢∀x∈A∀y∈Bφ↔∀z∈A∀w∈Bψ

Proof

Step Hyp Ref Expression
1 cbvral2vw.1 ⊢x=z→φ↔χ
2 cbvral2vw.2 ⊢y=w→χ↔ψ
3 1 ralbidv ⊢x=z→∀y∈Bφ↔∀y∈Bχ
4 3 cbvralvw ⊢∀x∈A∀y∈Bφ↔∀z∈A∀y∈Bχ
5 2 cbvralvw ⊢∀y∈Bχ↔∀w∈Bψ
6 5 ralbii ⊢∀z∈A∀y∈Bχ↔∀z∈A∀w∈Bψ
7 4 6 bitri ⊢∀x∈A∀y∈Bφ↔∀z∈A∀w∈Bψ