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) (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 ψ