# Metamath Proof Explorer

## Theorem rexxfrd2

Description: Transfer existence from a variable x to another variable y contained in expression A . Variant of rexxfrd . (Contributed by Alexander van der Vekens, 25-Apr-2018)

Ref Expression
Hypotheses ralxfrd2.1 ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to {A}\in {B}$
ralxfrd2.2 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}{x}={A}$
ralxfrd2.3 ${⊢}\left({\phi }\wedge {y}\in {C}\wedge {x}={A}\right)\to \left({\psi }↔{\chi }\right)$
Assertion rexxfrd2 ${⊢}{\phi }\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$

### Proof

Step Hyp Ref Expression
1 ralxfrd2.1 ${⊢}\left({\phi }\wedge {y}\in {C}\right)\to {A}\in {B}$
2 ralxfrd2.2 ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \exists {y}\in {C}\phantom{\rule{.4em}{0ex}}{x}={A}$
3 ralxfrd2.3 ${⊢}\left({\phi }\wedge {y}\in {C}\wedge {x}={A}\right)\to \left({\psi }↔{\chi }\right)$
4 3 notbid ${⊢}\left({\phi }\wedge {y}\in {C}\wedge {x}={A}\right)\to \left(¬{\psi }↔¬{\chi }\right)$
5 1 2 4 ralxfrd2 ${⊢}{\phi }\to \left(\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }↔\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}¬{\chi }\right)$
6 5 notbid ${⊢}{\phi }\to \left(¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }↔¬\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}¬{\chi }\right)$
7 dfrex2 ${⊢}\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }$
8 dfrex2 ${⊢}\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }↔¬\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}¬{\chi }$
9 6 7 8 3bitr4g ${⊢}{\phi }\to \left(\exists {x}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {y}\in {C}\phantom{\rule{.4em}{0ex}}{\chi }\right)$