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

Theorem f1oeq1 6022
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 5991 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6006 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 742 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 5794 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 5794 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 301 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  1-1wf1 5784  ontowfo 5785  1-1-ontowf1o 5786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-br 4575  df-opab 4635  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794
This theorem is referenced by:  f1oeq123d  6028  f1ocnvb  6045  f1orescnv  6047  resin  6053  f1ovi  6069  f1osng  6071  f1oresrab  6284  fsn  6290  fveqf1o  6432  isoeq1  6442  f1oexbi  6983  oacomf1o  7506  mapsn  7759  mapsnf1o3  7766  f1oen3g  7831  ensn1  7880  xpcomf1o  7908  omf1o  7922  enfixsn  7928  domss2  7978  php3  8005  isinf  8032  ssfi  8039  oef1o  8452  cnfcomlem  8453  cnfcom  8454  cnfcom2  8456  cnfcom3  8458  cnfcom3clem  8459  infxpenc  8698  infxpenc2lem2  8700  infxpenc2  8702  ackbij2lem2  8919  ackbij2  8922  canthp1lem2  9328  pwfseqlem5  9338  pwfseq  9339  seqf1olem2  12655  seqf1o  12656  hasheqf1oi  12951  hasheqf1oiOLD  12952  hashf1rn  12953  hashf1rnOLD  12954  hasheqf1od  12955  hashfacen  13044  wrd2f1tovbij  13494  summo  14238  fsum  14241  ackbijnn  14342  prodmo  14448  fprod  14453  bitsf1ocnv  14947  sadcaddlem  14960  unbenlem  15393  setcinv  16506  equivestrcsetc  16558  yonffthlem  16688  grplactcnv  17284  eqgen  17413  isgim  17470  elsymgbas2  17567  symg1bas  17582  cayleyth  17601  gsumval3eu  18071  gsumval3lem1  18072  gsumval3lem2  18073  islmim  18826  coe1mul2lem2  19402  znunithash  19674  uvcendim  19944  mdet0f1o  20157  tgpconcompeqg  21664  resinf1o  24000  efif1olem4  24009  logf1o  24029  relogf1o  24031  dvlog  24111  2lgslem1  24833  isismt  25144  nbgraf1o0  25738  cusgrafilem3  25772  wlknwwlknbij2  26005  wlkiswwlkbij2  26012  wwlkextbij  26024  wlknwwlknvbij  26031  clwwlkbij  26090  clwwlkvbij  26092  iseupa  26255  eupares  26265  eupap1  26266  frgrancvvdeqlem9  26331  numclwlk1lem2  26387  hoif  27800  rabfodom  28531  fresf1o  28618  fcobijfs  28692  fpwrelmapffs  28700  gsummpt2d  28915  indf1o  29216  eulerpartlem1  29559  eulerpartgbij  29564  eulerpart  29574  derangenlem  30210  subfacp1lem2a  30219  subfacp1lem3  30221  subfacp1lem5  30223  subfacp1lem6  30224  subfacp1  30225  f1omptsn  32160  poimirlem3  32382  poimirlem4  32383  poimirlem5  32384  poimirlem6  32385  poimirlem7  32386  poimirlem8  32387  poimirlem9  32388  poimirlem10  32389  poimirlem11  32390  poimirlem12  32391  poimirlem13  32392  poimirlem14  32393  poimirlem15  32394  poimirlem16  32395  poimirlem17  32396  poimirlem18  32397  poimirlem19  32398  poimirlem20  32399  poimirlem21  32400  poimirlem22  32401  poimirlem25  32404  poimirlem26  32405  poimirlem27  32406  poimirlem29  32408  poimirlem31  32410  isismty  32570  ismrer1  32607  isrngoiso  32747  islaut  34187  ispautN  34203  hvmap1o  35870  eldioph2lem1  36141  pwfi2f1o  36484  rfovcnvf1od  37118  clsneif1o  37222  neicvgf1o  37232  f1oeq1d  38158  mapsnd  38183  nbusgrf1o1  40597  cusgrfilem3  40672  1wlkisowwlkupgr  41076  wlknwwlksnbij2  41088  wlkwwlkbij2  41095  wwlksnextbij  41107  wlksnwwlknvbij  41113  clwwlksbij  41226  clwwlksvbij  41228  av-numclwlk1lem2  41526
  Copyright terms: Public domain W3C validator