Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 cbvfo.1 F x = y φ ψ
2 1 notbid F x = y ¬ φ ¬ ψ
3 2 cbvfo F : A onto B x A ¬ φ y B ¬ ψ
4 3 notbid F : A onto B ¬ x A ¬ φ ¬ y B ¬ ψ
5 dfrex2 x A φ ¬ x A ¬ φ
6 dfrex2 y B ψ ¬ y B ¬ ψ
7 4 5 6 3bitr4g F : A onto B x A φ y B ψ