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