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

Theorem f1oeq2d 6378
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 6372 . 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 1656  1-1-ontowf1o 6126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134
This theorem is referenced by:  f1osng  6422  f1o2sn  6663  fveqf1o  6817  oacomf1o  7917  marypha1lem  8614  oef1o  8879  cnfcomlem  8880  cnfcom2  8883  infxpenc  9161  pwfseqlem5  9807  pwfseq  9808  summolem3  14829  summo  14832  fsum  14835  prodmolem3  15043  prodmo  15046  fprod  15051  gsumvalx  17630  gsumpropd  17632  gsumpropd2lem  17633  gsumval3lem1  18666  gsumval3  18668  cncfcnvcn  23101  isismt  25853  f1ocnt  30102  erdsze2lem1  31727  ismtyval  34136  rngoisoval  34313  lautset  36152  pautsetN  36168  eldioph2lem1  38162  imasgim  38508  stoweidlem35  41040  stoweidlem39  41044  isomgreqve  42557
  Copyright terms: Public domain W3C validator