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

Theorem f1oeq2d 6781
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 6774 . 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-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504
This theorem is referenced by:  f1osng  6826  f1o2sn  7089  fveqf1o  7250  oacomf1o  8513  marypha1lem  9370  oef1o  9635  cnfcomlem  9636  cnfcom2  9639  infxpenc  9955  pwfseqlem5  10600  pwfseq  10601  summolem3  15600  summo  15603  fsum  15606  prodmolem3  15817  prodmo  15820  fprod  15825  gsumvalx  18532  gsumpropd  18534  gsumpropd2lem  18535  gsumval3lem1  19683  gsumval3  19685  cncfcnvcn  24291  isismt  27479  f1ocnt  31708  erdsze2lem1  33800  ismtyval  36262  rngoisoval  36439  lautset  38548  pautsetN  38564  sticksstones3  40559  sticksstones20  40577  eldioph2lem1  41086  imasgim  41430  stoweidlem35  44283  stoweidlem39  44287  isomgreqve  46024
  Copyright terms: Public domain W3C validator