# Metamath Proof Explorer

## Theorem cbvexfo

Description: Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997)

Ref Expression
Hypothesis cbvfo.1 ${⊢}{F}\left({x}\right)={y}\to \left({\phi }↔{\psi }\right)$
Assertion cbvexfo ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 cbvfo.1 ${⊢}{F}\left({x}\right)={y}\to \left({\phi }↔{\psi }\right)$
2 1 notbid ${⊢}{F}\left({x}\right)={y}\to \left(¬{\phi }↔¬{\psi }\right)$
3 2 cbvfo ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
4 3 notbid ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }\right)$
5 dfrex2 ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }$
6 dfrex2 ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 4 5 6 3bitr4g ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$