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

Metamath Proof Explorer

Theorem cbvrexw

Description: Rule used to change bound variables, using implicit substitution. Version of cbvrexfw with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

Ref Expression
Hypotheses cbvralw.1 ⊢ Ⅎ y φ
cbvralw.2 ⊢ Ⅎ x ψ
cbvralw.3 ⊢ x = y → φ ↔ ψ
Assertion cbvrexw ⊢ ∃ x ∈ A φ ↔ ∃ y ∈ A ψ

Proof

Step Hyp Ref Expression
1 cbvralw.1 ⊢ Ⅎ y φ
2 cbvralw.2 ⊢ Ⅎ x ψ
3 cbvralw.3 ⊢ x = y → φ ↔ ψ
4 nfcv ⊢ Ⅎ _ x A
5 nfcv ⊢ Ⅎ _ y A
6 4 5 1 2 3 cbvrexfw ⊢ ∃ x ∈ A φ ↔ ∃ y ∈ A ψ