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 ` x ) = y -> ( ph <-> ps ) )
Assertion	cbvfo	|- ( F : A -onto-> B -> ( A. x e. A ph <-> A. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		cbvfo.1	|- ( ( F ` x ) = y -> ( ph <-> ps ) )
2		fofn	|- ( F : A -onto-> B -> F Fn A )
3	1	bicomd	|- ( ( F ` x ) = y -> ( ps <-> ph ) )
4	3	eqcoms	|- ( y = ( F ` x ) -> ( ps <-> ph ) )
5	4	ralrn	|- ( F Fn A -> ( A. y e. ran F ps <-> A. x e. A ph ) )
6	2 5	syl	|- ( F : A -onto-> B -> ( A. y e. ran F ps <-> A. x e. A ph ) )
7		forn	|- ( F : A -onto-> B -> ran F = B )
8	7	raleqdv	|- ( F : A -onto-> B -> ( A. y e. ran F ps <-> A. y e. B ps ) )
9	6 8	bitr3d	|- ( F : A -onto-> B -> ( A. x e. A ph <-> A. y e. B ps ) )