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

Metamath Proof Explorer

Theorem cbvrexv2

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralv2.1 ⊢ x = y → ψ ↔ χ
cbvralv2.2 ⊢ x = y → A = B
Assertion cbvrexv2 ⊢ ∃ x ∈ A ψ ↔ ∃ y ∈ B χ

Proof

Step Hyp Ref Expression
1 cbvralv2.1 ⊢ x = y → ψ ↔ χ
2 cbvralv2.2 ⊢ x = y → A = B
3 nfcv ⊢ Ⅎ _ y A
4 nfcv ⊢ Ⅎ _ x B
5 nfv ⊢ Ⅎ y ψ
6 nfv ⊢ Ⅎ x χ
7 3 4 5 6 2 1 cbvrexcsf ⊢ ∃ x ∈ A ψ ↔ ∃ y ∈ B χ