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

Metamath Proof Explorer

Theorem f1eq123d

Description: Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses f1eq123d.1 
|- ( ph -> F = G )
f1eq123d.2 
|- ( ph -> A = B )
f1eq123d.3 
|- ( ph -> C = D )
Assertion f1eq123d 
|- ( ph -> ( F : A -1-1-> C <-> G : B -1-1-> D ) )

Proof

Step Hyp Ref Expression
1 f1eq123d.1 
 |-  ( ph -> F = G )
2 f1eq123d.2 
 |-  ( ph -> A = B )
3 f1eq123d.3 
 |-  ( ph -> C = D )
4 f1eq1 
 |-  ( F = G -> ( F : A -1-1-> C <-> G : A -1-1-> C ) )
5 1 4 syl 
 |-  ( ph -> ( F : A -1-1-> C <-> G : A -1-1-> C ) )
6 f1eq2 
 |-  ( A = B -> ( G : A -1-1-> C <-> G : B -1-1-> C ) )
7 2 6 syl 
 |-  ( ph -> ( G : A -1-1-> C <-> G : B -1-1-> C ) )
8 f1eq3 
 |-  ( C = D -> ( G : B -1-1-> C <-> G : B -1-1-> D ) )
9 3 8 syl 
 |-  ( ph -> ( G : B -1-1-> C <-> G : B -1-1-> D ) )
10 5 7 9 3bitrd 
 |-  ( ph -> ( F : A -1-1-> C <-> G : B -1-1-> D ) )