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 φ ψ
Assertion cbvfo F : A onto B x A φ y B ψ

Proof

Step Hyp Ref Expression
1 cbvfo.1 F x = y φ ψ
2 fofn F : A onto B F Fn A
3 1 bicomd F x = y ψ φ
4 3 eqcoms y = F x ψ φ
5 4 ralrn F Fn A y ran F ψ x A φ
6 2 5 syl F : A onto B y ran F ψ x A φ
7 forn F : A onto B ran F = B
8 7 raleqdv F : A onto B y ran F ψ y B ψ
9 6 8 bitr3d F : A onto B x A φ y B ψ