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

Theorem f1oeq1 6165
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 6134 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6149 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 747 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 5933 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 5933 . 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 1523  1-1wf1 5923  ontowfo 5924  1-1-ontowf1o 5925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933
This theorem is referenced by:  f1oeq123d  6171  f1ocnvb  6188  f1orescnv  6190  resin  6196  f1ovi  6213  f1osng  6215  f1oresrab  6435  fsn  6442  fveqf1o  6597  isoeq1  6607  f1oexbi  7158  oacomf1o  7690  mapsn  7941  mapsnf1o3  7948  f1oen3g  8013  ensn1  8061  xpcomf1o  8090  omf1o  8104  enfixsn  8110  domss2  8160  php3  8187  isinf  8214  ssfi  8221  oef1o  8633  cnfcomlem  8634  cnfcom  8635  cnfcom2  8637  cnfcom3  8639  cnfcom3clem  8640  infxpenc  8879  infxpenc2lem2  8881  infxpenc2  8883  ackbij2lem2  9100  ackbij2  9103  canthp1lem2  9513  pwfseqlem5  9523  pwfseq  9524  seqf1olem2  12881  seqf1o  12882  hasheqf1oi  13180  hashf1rn  13181  hasheqf1od  13182  hashfacen  13276  wrd2f1tovbij  13749  summo  14492  fsum  14495  ackbijnn  14604  prodmo  14710  fprod  14715  bitsf1ocnv  15213  sadcaddlem  15226  unbenlem  15659  setcinv  16787  equivestrcsetc  16839  yonffthlem  16969  grplactcnv  17565  eqgen  17694  isgim  17751  elsymgbas2  17847  symg1bas  17862  cayleyth  17881  gsumval3eu  18351  gsumval3lem1  18352  gsumval3lem2  18353  islmim  19110  coe1mul2lem2  19686  znunithash  19961  uvcendim  20234  mdet0f1o  20447  tgpconncompeqg  21962  resinf1o  24327  efif1olem4  24336  logf1o  24356  relogf1o  24358  dvlog  24442  2lgslem1  25164  isismt  25474  nbusgrf1o1  26316  cusgrfilem3  26409  wlkisowwlkupgr  26834  wlknwwlksnbij2  26846  wlkwwlkbij2  26853  wwlksnextbij  26865  wlksnwwlknvbij  26871  clwwlkbij  27015  clwwlkvbij  27088  clwwlkvbijOLD  27089  numclwlk1lem2  27350  hoif  28741  rabfodom  29470  fresf1o  29561  fcobijfs  29629  fpwrelmapffs  29637  gsummpt2d  29909  pmtridf1o  29984  indf1o  30214  eulerpartlem1  30557  eulerpartgbij  30562  eulerpart  30572  derangenlem  31279  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem5  31292  subfacp1lem6  31293  subfacp1  31294  f1omptsn  33314  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem9  33548  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem14  33553  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem29  33568  poimirlem31  33570  isismty  33730  ismrer1  33767  isrngoiso  33907  islaut  35687  ispautN  35703  hvmap1o  37369  eldioph2lem1  37640  pwfi2f1o  37983  rfovcnvf1od  38615  clsneif1o  38719  neicvgf1o  38729  f1oeq1d  39677  mapsnd  39702  sprbisymrel  42074  uspgrbispr  42084  uspgrbisymrelALT  42088
  Copyright terms: Public domain W3C validator