Metamath Proof Explorer

Theorem cbvrex2vw

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

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

Proof

Step Hyp Ref Expression
1 cbvrex2vw.1 ⊢ x = z → φ ↔ χ
2 cbvrex2vw.2 ⊢ y = w → χ ↔ ψ
3 1 rexbidv ⊢ x = z → ∃ y ∈ B φ ↔ ∃ y ∈ B χ
4 3 cbvrexvw ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ z ∈ A ∃ y ∈ B χ
5 2 cbvrexvw ⊢ ∃ y ∈ B χ ↔ ∃ w ∈ B ψ
6 5 rexbii ⊢ ∃ z ∈ A ∃ y ∈ B χ ↔ ∃ z ∈ A ∃ w ∈ B ψ
7 4 6 bitri ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ z ∈ A ∃ w ∈ B ψ