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

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

Proof of Theorem f1oeq2d
StepHypRef Expression
1 f1oeq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 f1oeq2 6596 . 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 209   = wceq 1538  1-1-ontowf1o 6342
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-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350
This theorem is referenced by:  f1osng  6646  f1o2sn  6895  fveqf1o  7051  oacomf1o  8187  marypha1lem  8894  oef1o  9158  cnfcomlem  9159  cnfcom2  9162  infxpenc  9442  pwfseqlem5  10083  pwfseq  10084  summolem3  15071  summo  15074  fsum  15077  prodmolem3  15287  prodmo  15290  fprod  15295  gsumvalx  17886  gsumpropd  17888  gsumpropd2lem  17889  gsumval3lem1  19025  gsumval3  19027  cncfcnvcn  23536  isismt  26334  f1ocnt  30539  erdsze2lem1  32510  ismtyval  35186  rngoisoval  35363  lautset  37326  pautsetN  37342  eldioph2lem1  39621  imasgim  39964  stoweidlem35  42607  stoweidlem39  42611  isomgreqve  44273
  Copyright terms: Public domain W3C validator