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

Theorem f1oeq3d 6388
Description: Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
f1oeq3d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
f1oeq3d (𝜑 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))

Proof of Theorem f1oeq3d
StepHypRef Expression
1 f1oeq3d.1 . 2 (𝜑𝐴 = 𝐵)
2 f1oeq3 6382 . 2 (𝐴 = 𝐵 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
31, 2syl 17 1 (𝜑 → (𝐹:𝐶1-1-onto𝐴𝐹:𝐶1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  1-1-ontowf1o 6134
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-in 3798  df-ss 3805  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142
This theorem is referenced by:  resdif  6411  f1osng  6431  f1oresrab  6659  fveqf1o  6829  isoini2  6861  oacomf1o  7929  mapsnf1o  8235  domss2  8407  wemapwe  8891  oef1o  8892  cnfcomlem  8893  cnfcom3  8898  cnfcom3clem  8899  infxpenc  9174  infxpenc2lem1  9175  infxpenc2  9178  ackbij2lem2  9397  hsmexlem1  9583  fsumss  14863  fsumcnv  14909  fprodss  15081  fprodcnv  15116  pwssnf1o  16544  catcisolem  17141  equivestrcsetc  17178  yoniso  17311  coe1mul2lem2  20034  usgrf1oedg  26553  wlkiswwlks2lem5  27222  clwwlkvbij  27515  clwwlkvbijOLD  27516  eupthresOLD  27618  eupthres  27619  eupthp1  27620  dimkerim  30441  poimirlem9  34039  sge0f1o  41516  nnfoctbdj  41590  f1oresf1o  42324  f1oresf1o2  42325  ushrisomgr  42747
  Copyright terms: Public domain W3C validator