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

Theorem f1oeq2 6290
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 6258 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴1-1𝐶𝐹:𝐵1-1𝐶))
2 foeq2 6274 . . 3 (𝐴 = 𝐵 → (𝐹:𝐴onto𝐶𝐹:𝐵onto𝐶))
31, 2anbi12d 749 . 2 (𝐴 = 𝐵 → ((𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶) ↔ (𝐹:𝐵1-1𝐶𝐹:𝐵onto𝐶)))
4 df-f1o 6056 . 2 (𝐹:𝐴1-1-onto𝐶 ↔ (𝐹:𝐴1-1𝐶𝐹:𝐴onto𝐶))
5 df-f1o 6056 . 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 383   = wceq 1632  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056
This theorem is referenced by:  f1oeq23  6292  f1oeq123d  6295  resin  6320  f1osng  6339  f1o2sn  6572  fveqf1o  6721  isoeq4  6734  oacomf1o  7816  bren  8132  f1dmvrnfibi  8417  marypha1lem  8506  oef1o  8770  cnfcomlem  8771  cnfcom  8772  cnfcom2  8774  infxpenc  9051  infxpenc2  9055  pwfseqlem5  9697  pwfseq  9698  summolem3  14664  summo  14667  fsum  14670  fsumf1o  14673  sumsnf  14692  sumsn  14694  prodmolem3  14882  prodmo  14885  fprod  14890  fprodf1o  14895  prodsn  14911  prodsnf  14913  gsumvalx  17491  gsumpropd  17493  gsumpropd2lem  17494  gsumval3lem1  18526  gsumval3  18528  znhash  20129  znunithash  20135  imasf1oxms  22515  cncfcnvcn  22945  wlksnwwlknvbij  27047  clwwlkvbij  27283  clwwlkvbijOLD  27284  eupthp1  27389  f1ocnt  29889  derangval  31477  subfacp1lem2a  31490  subfacp1lem3  31492  subfacp1lem5  31494  erdsze2lem1  31513  ismtyval  33930  rngoisoval  34107  lautset  35889  pautsetN  35905  eldioph2lem1  37843  imasgim  38190  sumsnd  39702  f1oeq2d  39878  stoweidlem35  40773  stoweidlem39  40777  uspgrsprfo  42284
  Copyright terms: Public domain W3C validator