# Metamath Proof Explorer

## Theorem cbvfo

Description: Change bound variable between domain and range of function. (Contributed by NM, 23-Feb-1997) (Proof shortened by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypothesis cbvfo.1 ${⊢}{F}\left({x}\right)={y}\to \left({\phi }↔{\psi }\right)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 cbvfo.1 ${⊢}{F}\left({x}\right)={y}\to \left({\phi }↔{\psi }\right)$
2 fofn ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to {F}Fn{A}$
3 1 bicomd ${⊢}{F}\left({x}\right)={y}\to \left({\psi }↔{\phi }\right)$
4 3 eqcoms ${⊢}{y}={F}\left({x}\right)\to \left({\psi }↔{\phi }\right)$
5 4 ralrn ${⊢}{F}Fn{A}\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
6 2 5 syl ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
7 forn ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \mathrm{ran}{F}={B}$
8 7 raleqdv ${⊢}{F}:{A}\underset{onto}{⟶}{B}\to \left(\forall {y}\in \mathrm{ran}{F}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
9 6 8 bitr3d ${⊢}{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)$