# Metamath Proof Explorer

## Theorem cbvrexvw

Description: Change the bound variable of a restricted existential quantifier using implicit substitution. Version of cbvrexv with a disjoint variable condition, which does not require ax-10 , ax-11 , ax-12 , ax-13 . (Contributed by NM, 2-Jun-1998) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypothesis cbvralvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvrexvw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 cbvralvw.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 eleq1w ${⊢}{x}={y}\to \left({x}\in {A}↔{y}\in {A}\right)$
3 2 1 anbi12d ${⊢}{x}={y}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({y}\in {A}\wedge {\psi }\right)\right)$
4 3 cbvexvw ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
5 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
6 df-rex ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
7 4 5 6 3bitr4i ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$