MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1eq123d Structured version   Unicode version

Theorem f1eq123d 5825
Description: Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypotheses
Ref Expression
f1eq123d.1  |-  ( ph  ->  F  =  G )
f1eq123d.2  |-  ( ph  ->  A  =  B )
f1eq123d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
f1eq123d  |-  ( ph  ->  ( F : A -1-1-> C  <-> 
G : B -1-1-> D
) )

Proof of Theorem f1eq123d
StepHypRef Expression
1 f1eq123d.1 . . 3  |-  ( ph  ->  F  =  G )
2 f1eq1 5790 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> C  <->  G : A -1-1-> C ) )
31, 2syl 17 . 2  |-  ( ph  ->  ( F : A -1-1-> C  <-> 
G : A -1-1-> C
) )
4 f1eq123d.2 . . 3  |-  ( ph  ->  A  =  B )
5 f1eq2 5791 . . 3  |-  ( A  =  B  ->  ( G : A -1-1-> C  <->  G : B -1-1-> C ) )
64, 5syl 17 . 2  |-  ( ph  ->  ( G : A -1-1-> C  <-> 
G : B -1-1-> C
) )
7 f1eq123d.3 . . 3  |-  ( ph  ->  C  =  D )
8 f1eq3 5792 . . 3  |-  ( C  =  D  ->  ( G : B -1-1-> C  <->  G : B -1-1-> D ) )
97, 8syl 17 . 2  |-  ( ph  ->  ( G : B -1-1-> C  <-> 
G : B -1-1-> D
) )
103, 6, 93bitrd 283 1  |-  ( ph  ->  ( F : A -1-1-> C  <-> 
G : B -1-1-> D
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   -1-1->wf1 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785  df-v 3084  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4423  df-opab 4482  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605
This theorem is referenced by:  fthf1  15819  cofth  15837  istrkgld  24503  istrkg2ld  24504  isushgra  25024  usgraeq12d  25085  usgra0v  25094  usgra1v  25113  usgrares1  25134  2spontn0vne  25611  aciunf1  28265  isushgr  38865  isuspgr  38920  isusgr  38921  usgrop  38931  ausgrusgrb  38933  ausgrusgri  38936  usgrres  38949  usgr0e  38980  uspgr1  38985  usgrexmpl  38997  usgrres1  39008  usgra2pthspth  39057  isushgrALTV  39071  usgedgleord  39123  isfusgra  39128  usgresvm1  39147  usgresvm1ALT  39151
  Copyright terms: Public domain W3C validator