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

Theorem f1oeq2d 6819
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 6812 . 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 1533  1-1-ontowf1o 6532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540
This theorem is referenced by:  f1osng  6864  f1o2sn  7132  fveqf1o  7293  oacomf1o  8560  marypha1lem  9423  oef1o  9688  cnfcomlem  9689  cnfcom2  9692  infxpenc  10008  pwfseqlem5  10653  pwfseq  10654  summolem3  15656  summo  15659  fsum  15662  prodmolem3  15873  prodmo  15876  fprod  15881  gsumvalx  18598  gsumpropd  18600  gsumpropd2lem  18601  gsumval3lem1  19814  gsumval3  19816  cncfcnvcn  24767  isismt  28220  f1ocnt  32448  erdsze2lem1  34649  ismtyval  37124  rngoisoval  37301  lautset  39409  pautsetN  39425  sticksstones3  41423  sticksstones20  41441  eldioph2lem1  41953  imasgim  42297  stoweidlem35  45202  stoweidlem39  45206  isomgreqve  46944
  Copyright terms: Public domain W3C validator