Metamath Proof Explorer

Theorem cbvrex2v

Description: Change bound variables of double restricted universal quantification, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrex2vw when possible. (Contributed by FL, 2-Jul-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvrex2v.1 ⊢ x = z → φ ↔ χ
2 cbvrex2v.2 ⊢ y = w → χ ↔ ψ
3 1 rexbidv ⊢ x = z → ∃ y ∈ B φ ↔ ∃ y ∈ B χ
4 3 cbvrexv ⊢ ∃ x ∈ A ∃ y ∈ B φ ↔ ∃ z ∈ A ∃ y ∈ B χ
5 2 cbvrexv ⊢ ∃ 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 ψ