Theorem cbvexfo

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

	Ref	Expression
Hypothesis	cbvfo.1	|- ( ( F ` x ) = y -> ( ph <-> ps ) )
Assertion	cbvexfo	|- ( F : A -onto-> B -> ( E. x e. A ph <-> E. y e. B ps ) )

Proof

Step	Hyp	Ref	Expression
1		cbvfo.1	|- ( ( F ` x ) = y -> ( ph <-> ps ) )
2	1	notbid	|- ( ( F ` x ) = y -> ( -. ph <-> -. ps ) )
3	2	cbvfo	|- ( F : A -onto-> B -> ( A. x e. A -. ph <-> A. y e. B -. ps ) )
4	3	notbid	|- ( F : A -onto-> B -> ( -. A. x e. A -. ph <-> -. A. y e. B -. ps ) )
5		dfrex2	|- ( E. x e. A ph <-> -. A. x e. A -. ph )
6		dfrex2	|- ( E. y e. B ps <-> -. A. y e. B -. ps )
7	4 5 6	3bitr4g	|- ( F : A -onto-> B -> ( E. x e. A ph <-> E. y e. B ps ) )