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

Theorem f1oeq1 6114
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 6083 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6098 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 746 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 5883 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 5883 . 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 1481  1-1wf1 5873  ontowfo 5874  1-1-ontowf1o 5875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883
This theorem is referenced by:  f1oeq123d  6120  f1ocnvb  6137  f1orescnv  6139  resin  6145  f1ovi  6162  f1osng  6164  f1oresrab  6381  fsn  6387  fveqf1o  6542  isoeq1  6552  f1oexbi  7101  oacomf1o  7630  mapsn  7884  mapsnf1o3  7891  f1oen3g  7956  ensn1  8005  xpcomf1o  8034  omf1o  8048  enfixsn  8054  domss2  8104  php3  8131  isinf  8158  ssfi  8165  oef1o  8580  cnfcomlem  8581  cnfcom  8582  cnfcom2  8584  cnfcom3  8586  cnfcom3clem  8587  infxpenc  8826  infxpenc2lem2  8828  infxpenc2  8830  ackbij2lem2  9047  ackbij2  9050  canthp1lem2  9460  pwfseqlem5  9470  pwfseq  9471  seqf1olem2  12824  seqf1o  12825  hasheqf1oi  13123  hasheqf1oiOLD  13124  hashf1rn  13125  hashf1rnOLD  13126  hasheqf1od  13127  hashfacen  13221  wrd2f1tovbij  13684  summo  14429  fsum  14432  ackbijnn  14541  prodmo  14647  fprod  14652  bitsf1ocnv  15147  sadcaddlem  15160  unbenlem  15593  setcinv  16721  equivestrcsetc  16773  yonffthlem  16903  grplactcnv  17499  eqgen  17628  isgim  17685  elsymgbas2  17782  symg1bas  17797  cayleyth  17816  gsumval3eu  18286  gsumval3lem1  18287  gsumval3lem2  18288  islmim  19043  coe1mul2lem2  19619  znunithash  19894  uvcendim  20167  mdet0f1o  20380  tgpconncompeqg  21896  resinf1o  24263  efif1olem4  24272  logf1o  24292  relogf1o  24294  dvlog  24378  2lgslem1  25100  isismt  25410  nbusgrf1o1  26253  cusgrfilem3  26334  wlkisowwlkupgr  26747  wlknwwlksnbij2  26759  wlkwwlkbij2  26766  wwlksnextbij  26778  wlksnwwlknvbij  26784  clwwlksbij  26900  clwwlksvbij  26902  numclwlk1lem2  27201  hoif  28583  rabfodom  29316  fresf1o  29406  fcobijfs  29475  fpwrelmapffs  29483  gsummpt2d  29755  pmtridf1o  29830  indf1o  30060  eulerpartlem1  30403  eulerpartgbij  30408  eulerpart  30418  derangenlem  31127  subfacp1lem2a  31136  subfacp1lem3  31138  subfacp1lem5  31140  subfacp1lem6  31141  subfacp1  31142  f1omptsn  33155  poimirlem3  33383  poimirlem4  33384  poimirlem5  33385  poimirlem6  33386  poimirlem7  33387  poimirlem8  33388  poimirlem9  33389  poimirlem10  33390  poimirlem11  33391  poimirlem12  33392  poimirlem13  33393  poimirlem14  33394  poimirlem15  33395  poimirlem16  33396  poimirlem17  33397  poimirlem18  33398  poimirlem19  33399  poimirlem20  33400  poimirlem21  33401  poimirlem22  33402  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  poimirlem29  33409  poimirlem31  33411  isismty  33571  ismrer1  33608  isrngoiso  33748  islaut  35188  ispautN  35204  hvmap1o  36871  eldioph2lem1  37142  pwfi2f1o  37485  rfovcnvf1od  38118  clsneif1o  38222  neicvgf1o  38232  f1oeq1d  39179  mapsnd  39204  sprbisymrel  41514  uspgrbispr  41524  uspgrbisymrelALT  41528
  Copyright terms: Public domain W3C validator