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

Theorem f1oeq1 5543
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )

Proof of Theorem f1oeq1
StepHypRef Expression
1 f1eq1 5512 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5527 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 691 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5341 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5341 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 279 1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1642   -1-1->wf1 5331   -onto->wfo 5332   -1-1-onto->wf1o 5333
This theorem is referenced by:  f1oeq123d  5549  f1ocnvb  5566  f1orescnv  5568  resin  5575  f1ovi  5592  f1osng  5594  f1oprswap  5595  fsn  5776  fveqf1o  5890  isoeq1  5900  oacomf1o  6647  mapsn  6894  mapsnf1o3  6901  f1oen3g  6962  ensn1  7010  xpcomf1o  7036  omf1o  7050  domss2  7105  php3  7132  isinf  7161  ssfi  7168  oef1o  7488  cnfcomlem  7489  cnfcom  7490  cnfcom2  7492  cnfcom3  7494  cnfcom3clem  7495  infxpenc  7732  infxpenc2lem2  7734  infxpenc2  7736  ackbij2lem2  7953  ackbij2  7956  canthp1lem2  8362  pwfseqlem5  8372  pwfseq  8373  seqf1olem2  11175  seqf1o  11176  hashfacen  11482  summo  12281  fsum  12284  ackbijnn  12377  bitsf1ocnv  12726  sadcaddlem  12739  unbenlem  13046  setcinv  14015  yonffthlem  14149  grplactcnv  14657  eqgen  14763  isgim  14819  elsymgbas2  14866  cayleyth  14883  gsumval3eu  15283  gsumval3  15284  islmim  15908  coe1mul2lem2  16438  znunithash  16618  tgpconcompeqg  17890  resinf1o  19999  efif1olem4  20008  logf1o  20023  relogf1o  20025  dvlog  20103  hoif  22442  indf1o  23687  derangenlem  24106  subfacp1lem2a  24115  subfacp1lem3  24117  subfacp1lem5  24119  subfacp1lem6  24120  subfacp1  24121  iseupa  24285  eupares  24303  eupap1  24304  elgiso  24407  prodmo  24563  fprod  24568  isismty  25848  ismrer1  25885  isrngoiso  25932  eldioph2lem1  26162  enfixsn  26580  pwfi2f1o  26583  hasheqf1oi  27476  nbgraf1o0  27602  frgrancvvdeqlem9  27857  islaut  30324  ispautN  30340  hvmap1o  32005
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341
  Copyright terms: Public domain W3C validator