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

Theorem f1oeq3d 6782
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 6775 . 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 205   = wceq 1542  1-1-ontowf1o 6496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  resdif  6806  f1osng  6826  f1oresrab  7074  fveqf1o  7250  isoini2  7285  oacomf1o  8513  mapsnf1o  8878  domss2  9081  dif1enlem  9101  dif1enlemOLD  9102  infn0  9252  wemapwe  9634  oef1o  9635  cnfcomlem  9636  cnfcom3  9641  cnfcom3clem  9642  infxpenc  9955  infxpenc2lem1  9956  infxpenc2  9959  ackbij2lem2  10177  hsmexlem1  10363  fsumss  15611  fsumcnv  15659  fprodss  15832  fprodcnv  15867  pwssnf1o  17381  catcisolem  17997  equivestrcsetc  18041  yoniso  18175  gsumpropd  18534  gsumpropd2lem  18535  xpsmnd  18597  xpsgrp  18867  gsumval3lem1  19683  gsumval3lem2  19684  gsumcom2  19753  coe1mul2lem2  21642  scmatrngiso  21888  m2cpmrngiso  22110  cncfcnvcn  24291  isismt  27479  usgrf1oedg  28158  wlkiswwlks2lem5  28821  clwwlkvbij  29060  eupthres  29162  eupthp1  29163  cycpmconjvlem  31993  tocyccntz  31996  ghmqusker  32201  dimkerim  32325  poimirlem4  36085  poimirlem9  36090  rngoisoval  36439  frlmsnic  40731  sge0f1o  44630  nnfoctbdj  44704  f1oresf1o  45529  ushrisomgr  46040
  Copyright terms: Public domain W3C validator