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

Theorem f1oeq1 6597
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 6563 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6579 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 630 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6355 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6355 . 2 (𝐺:𝐴1-1-onto𝐵 ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵))
63, 4, 53bitr4g 315 1 (𝐹 = 𝐺 → (𝐹:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  1-1wf1 6345  ontowfo 6346  1-1-ontowf1o 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355
This theorem is referenced by:  f1oeq123d  6603  f1ocnvb  6621  f1orescnv  6623  resin  6629  f1ovi  6646  f1osng  6648  f1oresrab  6881  fsn  6889  fveqf1o  7049  isoeq1  7059  f1oexbi  7622  oacomf1o  8180  mapsnd  8438  mapsnf1o3  8447  f1oen3g  8513  ensn1  8561  xpcomf1o  8594  omf1o  8608  enfixsn  8614  domss2  8664  php3  8691  isinf  8719  ssfi  8726  oef1o  9149  cnfcomlem  9150  cnfcom  9151  cnfcom2  9153  cnfcom3  9155  cnfcom3clem  9156  infxpenc  9432  infxpenc2lem2  9434  infxpenc2  9436  ackbij2lem2  9650  ackbij2  9653  canthp1lem2  10063  pwfseqlem5  10073  pwfseq  10074  seqf1olem2  13398  seqf1o  13399  hasheqf1oi  13700  hashf1rn  13701  hasheqf1od  13702  hashfacen  13800  wrd2f1tovbij  14312  summo  15062  fsum  15065  ackbijnn  15171  prodmo  15278  fprod  15283  bitsf1ocnv  15781  sadcaddlem  15794  unbenlem  16232  setcinv  17338  equivestrcsetc  17390  yonffthlem  17520  grplactcnv  18140  eqgen  18271  isgim  18340  elsymgbas2  18437  symg1bas  18453  cayleyth  18472  gsumval3eu  18953  gsumval3lem1  18954  gsumval3lem2  18955  islmim  19763  coe1mul2lem2  20364  znunithash  20639  uvcendim  20919  mdet0f1o  21130  tgpconncompeqg  22647  resinf1o  25047  efif1olem4  25056  logf1o  25075  relogf1o  25077  dvlog  25161  2lgslem1  25897  isismt  26247  nbusgrf1o1  27079  cusgrfilem3  27166  wwlksnextbij  27607  wlksnwwlknvbij  27614  clwwlkvbij  27819  hoif  29458  rabfodom  30193  fresf1o  30304  fcobijfs  30385  fpwrelmapffs  30396  s2f1  30548  gsummpt2d  30614  pmtridf1o  30663  cycpmconjslem2  30724  indf1o  31182  eulerpartlem1  31524  eulerpartgbij  31529  eulerpart  31539  derangenlem  32315  subfacp1lem2a  32324  subfacp1lem3  32326  subfacp1lem5  32328  subfacp1lem6  32329  subfacp1  32330  f1omptsn  34500  poimirlem3  34776  poimirlem4  34777  poimirlem5  34778  poimirlem6  34779  poimirlem7  34780  poimirlem8  34781  poimirlem9  34782  poimirlem10  34783  poimirlem11  34784  poimirlem12  34785  poimirlem13  34786  poimirlem14  34787  poimirlem15  34788  poimirlem16  34789  poimirlem17  34790  poimirlem18  34791  poimirlem19  34792  poimirlem20  34793  poimirlem21  34794  poimirlem22  34795  poimirlem25  34798  poimirlem26  34799  poimirlem27  34800  poimirlem29  34802  poimirlem31  34804  isismty  34960  ismrer1  34997  isrngoiso  35137  islaut  37099  ispautN  37115  hvmap1o  38779  eldioph2lem1  39235  pwfi2f1o  39574  rfovcnvf1od  40228  clsneif1o  40332  neicvgf1o  40342  f1oeq1d  41313  fundcmpsurbijinjpreimafv  43444  sprbisymrel  43538  prproropen  43547  isomgreqve  43867  isomushgr  43868  isomuspgrlem2  43875  isomgrsym  43878  isomgrtr  43881  ushrisomgr  43883  uspgrbispr  43903  uspgrbisymrelALT  43907  rrx2xpreen  44634
  Copyright terms: Public domain W3C validator