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

Theorem f1eq123d 6589
Description: Equality deduction for one-to-one functions. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypotheses
Ref Expression
f1eq123d.1 (𝜑𝐹 = 𝐺)
f1eq123d.2 (𝜑𝐴 = 𝐵)
f1eq123d.3 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
f1eq123d (𝜑 → (𝐹:𝐴1-1𝐶𝐺:𝐵1-1𝐷))

Proof of Theorem f1eq123d
StepHypRef Expression
1 f1eq123d.1 . . 3 (𝜑𝐹 = 𝐺)
2 f1eq1 6551 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐶𝐺:𝐴1-1𝐶))
31, 2syl 17 . 2 (𝜑 → (𝐹:𝐴1-1𝐶𝐺:𝐴1-1𝐶))
4 f1eq123d.2 . . 3 (𝜑𝐴 = 𝐵)
5 f1eq2 6552 . . 3 (𝐴 = 𝐵 → (𝐺:𝐴1-1𝐶𝐺:𝐵1-1𝐶))
64, 5syl 17 . 2 (𝜑 → (𝐺:𝐴1-1𝐶𝐺:𝐵1-1𝐶))
7 f1eq123d.3 . . 3 (𝜑𝐶 = 𝐷)
8 f1eq3 6553 . . 3 (𝐶 = 𝐷 → (𝐺:𝐵1-1𝐶𝐺:𝐵1-1𝐷))
97, 8syl 17 . 2 (𝜑 → (𝐺:𝐵1-1𝐶𝐺:𝐵1-1𝐷))
103, 6, 93bitrd 308 1 (𝜑 → (𝐹:𝐴1-1𝐶𝐺:𝐵1-1𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  1-1wf1 6333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141  df-v 3481  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-br 5048  df-opab 5110  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341
This theorem is referenced by:  f10d  6629  fthf1  17176  cofth  17194  istrkgld  26242  istrkg2ld  26243  isushgr  26843  isuspgr  26934  isusgr  26935  isuspgrop  26943  isusgrop  26944  ausgrusgrb  26947  ausgrusgri  26950  usgrstrrepe  27014  uspgr1e  27023  usgrexmpl  27042  usgrres1  27094  usgrexi  27220  uspgr2wlkeq  27424  usgr2trlncl  27538  aciunf1  30405  pfxf1  30615  s1f1  30616  tocycfv  30769  tocycf  30777  tocyc01  30778  cycpmco2f1  30784  cycpmco2rn  30785  cycpmco2lem1  30786  cycpmco2lem2  30787  cycpmco2lem3  30788  cycpmco2lem4  30789  cycpmco2lem5  30790  cycpmco2lem6  30791  cycpmco2lem7  30792  cycpmco2  30793  cycpm3cl2  30796  cycpmconjv  30802  tocyccntz  30804  cyc3evpm  30810  cycpmgcl  30813  cycpmconjslem2  30815  cyc3conja  30817  dimkerim  31044  f1resfz0f1d  32379  fundcmpsurinjALT  43771
  Copyright terms: Public domain W3C validator