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 \leftrightarrow \psi \right)$$
Assertion	cbvfo	$$⊢F:A\underset{onto}{⟶}B\to \left(\forall x\in A\phi \leftrightarrow \forall y\in B\psi \right)$$

Proof

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