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

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

Proof of Theorem f1oeq1
StepHypRef Expression
1 f1eq1 6320 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6336 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 618 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6117 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6117 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 305 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  1-1wf1 6107  ontowfo 6108  1-1-ontowf1o 6109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117
This theorem is referenced by:  f1oeq123d  6358  f1ocnvb  6375  f1orescnv  6377  resin  6383  f1ovi  6400  f1osng  6402  f1oresrab  6626  fsn  6634  fveqf1o  6790  isoeq1  6800  f1oexbi  7355  oacomf1o  7891  mapsnd  8143  mapsnf1o3  8152  f1oen3g  8217  ensn1  8265  xpcomf1o  8297  omf1o  8311  enfixsn  8317  domss2  8367  php3  8394  isinf  8421  ssfi  8428  oef1o  8851  cnfcomlem  8852  cnfcom  8853  cnfcom2  8855  cnfcom3  8857  cnfcom3clem  8858  infxpenc  9133  infxpenc2lem2  9135  infxpenc2  9137  ackbij2lem2  9356  ackbij2  9359  canthp1lem2  9769  pwfseqlem5  9779  pwfseq  9780  seqf1olem2  13083  seqf1o  13084  hasheqf1oi  13379  hashf1rn  13380  hasheqf1od  13381  hashfacen  13474  wrd2f1tovbij  13947  summo  14690  fsum  14693  ackbijnn  14801  prodmo  14906  fprod  14911  bitsf1ocnv  15404  sadcaddlem  15417  unbenlem  15848  setcinv  16963  equivestrcsetc  17016  yonffthlem  17146  grplactcnv  17742  eqgen  17868  isgim  17925  elsymgbas2  18021  symg1bas  18036  cayleyth  18055  gsumval3eu  18525  gsumval3lem1  18526  gsumval3lem2  18527  islmim  19288  coe1mul2lem2  19865  znunithash  20139  uvcendim  20416  mdet0f1o  20630  tgpconncompeqg  22148  resinf1o  24519  efif1olem4  24528  logf1o  24547  relogf1o  24549  dvlog  24633  2lgslem1  25355  isismt  25665  nbusgrf1o1  26510  cusgrfilem3  26603  wlknwwlksnbij2OLD  27042  wlkwwlkbij2OLD  27049  wwlksnextbij  27061  wlksnwwlknvbij  27067  wlksnwwlknvbijOLD  27068  clwwlkvbij  27304  clwwlkvbijOLDOLD  27305  clwwlkvbijOLD  27306  numclwwlk1lem2OLD  27562  hoif  28963  rabfodom  29691  fresf1o  29782  fcobijfs  29850  fpwrelmapffs  29858  gsummpt2d  30128  pmtridf1o  30203  indf1o  30433  eulerpartlem1  30776  eulerpartgbij  30781  eulerpart  30791  derangenlem  31497  subfacp1lem2a  31506  subfacp1lem3  31508  subfacp1lem5  31510  subfacp1lem6  31511  subfacp1  31512  f1omptsn  33519  poimirlem3  33743  poimirlem4  33744  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem9  33749  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem13  33753  poimirlem14  33754  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem25  33765  poimirlem26  33766  poimirlem27  33767  poimirlem29  33769  poimirlem31  33771  isismty  33929  ismrer1  33966  isrngoiso  34106  islaut  35881  ispautN  35897  hvmap1o  37561  eldioph2lem1  37842  pwfi2f1o  38184  rfovcnvf1od  38815  clsneif1o  38919  neicvgf1o  38929  f1oeq1d  39869  sprbisymrel  42334  uspgrbispr  42344  uspgrbisymrelALT  42348
  Copyright terms: Public domain W3C validator