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

Theorem f1oeq1 6598
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 6564 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴1-1𝐵𝐺:𝐴1-1𝐵))
2 foeq1 6580 . . 3 (𝐹 = 𝐺 → (𝐹:𝐴onto𝐵𝐺:𝐴onto𝐵))
31, 2anbi12d 630 . 2 (𝐹 = 𝐺 → ((𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵) ↔ (𝐺:𝐴1-1𝐵𝐺:𝐴onto𝐵)))
4 df-f1o 6356 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
5 df-f1o 6356 . 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 6346  ontowfo 6347  1-1-ontowf1o 6348
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356
This theorem is referenced by:  f1oeq123d  6604  f1ocnvb  6622  f1orescnv  6624  resin  6630  f1ovi  6647  f1osng  6649  f1oresrab  6882  fsn  6890  fveqf1o  7049  isoeq1  7059  f1oexbi  7621  oacomf1o  8181  mapsnd  8439  mapsnf1o3  8448  f1oen3g  8514  ensn1  8562  xpcomf1o  8595  omf1o  8609  enfixsn  8615  domss2  8665  php3  8692  isinf  8720  ssfi  8727  oef1o  9150  cnfcomlem  9151  cnfcom  9152  cnfcom2  9154  cnfcom3  9156  cnfcom3clem  9157  infxpenc  9433  infxpenc2lem2  9435  infxpenc2  9437  ackbij2lem2  9651  ackbij2  9654  canthp1lem2  10064  pwfseqlem5  10074  pwfseq  10075  seqf1olem2  13400  seqf1o  13401  hasheqf1oi  13702  hashf1rn  13703  hasheqf1od  13704  hashfacen  13802  wrd2f1tovbij  14314  summo  15064  fsum  15067  ackbijnn  15173  prodmo  15280  fprod  15285  bitsf1ocnv  15783  sadcaddlem  15796  unbenlem  16234  setcinv  17340  equivestrcsetc  17392  yonffthlem  17522  grplactcnv  18142  eqgen  18273  isgim  18342  elsymgbas2  18439  symg1bas  18455  cayleyth  18474  gsumval3eu  18955  gsumval3lem1  18956  gsumval3lem2  18957  islmim  19765  coe1mul2lem2  20366  znunithash  20641  uvcendim  20921  mdet0f1o  21132  tgpconncompeqg  22649  resinf1o  25047  efif1olem4  25056  logf1o  25075  relogf1o  25077  dvlog  25161  2lgslem1  25898  isismt  26248  nbusgrf1o1  27080  cusgrfilem3  27167  wwlksnextbij  27608  wlksnwwlknvbij  27615  clwwlkvbij  27820  hoif  29459  rabfodom  30194  fresf1o  30305  fcobijfs  30386  fpwrelmapffs  30397  s2f1  30549  gsummpt2d  30615  pmtridf1o  30664  cycpmconjslem2  30725  indf1o  31183  eulerpartlem1  31525  eulerpartgbij  31530  eulerpart  31540  derangenlem  32316  subfacp1lem2a  32325  subfacp1lem3  32327  subfacp1lem5  32329  subfacp1lem6  32330  subfacp1  32331  f1omptsn  34501  poimirlem3  34777  poimirlem4  34778  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem9  34783  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  poimirlem29  34803  poimirlem31  34805  isismty  34962  ismrer1  34999  isrngoiso  35139  islaut  37101  ispautN  37117  hvmap1o  38781  eldioph2lem1  39237  pwfi2f1o  39576  rfovcnvf1od  40230  clsneif1o  40334  neicvgf1o  40344  f1oeq1d  41317  sprbisymrel  43508  prproropen  43517  isomgreqve  43837  isomushgr  43838  isomuspgrlem2  43845  isomgrsym  43848  isomgrtr  43851  ushrisomgr  43853  uspgrbispr  43873  uspgrbisymrelALT  43877  rrx2xpreen  44604
  Copyright terms: Public domain W3C validator