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

Theorem f1oeq2 6085
 Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq2 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))

Proof of Theorem f1oeq2
StepHypRef Expression
1 f1eq2 6054 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6069 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 746 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 5854 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 5854 . 2 (𝐹:𝐵1-1-onto𝐶 ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶))
63, 4, 53bitr4g 303 1 (𝐴 = 𝐵 → (𝐹:𝐴1-1-onto𝐶𝐹:𝐵1-1-onto𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  –1-1→wf1 5844  –onto→wfo 5845  –1-1-onto→wf1o 5846 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854 This theorem is referenced by:  f1oeq23  6087  f1oeq123d  6090  resin  6115  f1osng  6134  f1o2sn  6362  fveqf1o  6511  isoeq4  6524  oacomf1o  7590  bren  7908  f1dmvrnfibi  8194  marypha1lem  8283  oef1o  8539  cnfcomlem  8540  cnfcom  8541  cnfcom2  8543  infxpenc  8785  infxpenc2  8789  pwfseqlem5  9429  pwfseq  9430  summolem3  14378  summo  14381  fsum  14384  fsumf1o  14387  sumsn  14405  prodmolem3  14588  prodmo  14591  fprod  14596  fprodf1o  14601  prodsn  14617  prodsnf  14619  gsumvalx  17191  gsumpropd  17193  gsumpropd2lem  17194  gsumval3lem1  18227  gsumval3  18229  znhash  19826  znunithash  19832  imasf1oxms  22204  cncfcnvcn  22632  wlksnwwlknvbij  26672  clwwlksvbij  26788  eupthp1  26942  f1ocnt  29400  derangval  30857  subfacp1lem2a  30870  subfacp1lem3  30872  subfacp1lem5  30874  erdsze2lem1  30893  ismtyval  33231  rngoisoval  33408  lautset  34848  pautsetN  34864  eldioph2lem1  36803  imasgim  37150  sumsnd  38668  f1oeq2d  38835  sumsnf  39205  stoweidlem35  39559  stoweidlem39  39563  uspgrsprfo  41044
 Copyright terms: Public domain W3C validator