This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ` 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 ) )