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

Theorem f1oeq1 5668
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 5637 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5652 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 693 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5464 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5464 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 281 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 178    /\ wa 360    = wceq 1653   -1-1->wf1 5454   -onto->wfo 5455   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1oeq123d  5674  f1ocnvb  5691  f1orescnv  5693  resin  5700  f1ovi  5717  f1osng  5719  fsn  5909  fveqf1o  6032  isoeq1  6042  oacomf1o  6811  mapsn  7058  mapsnf1o3  7065  f1oen3g  7126  ensn1  7174  xpcomf1o  7200  omf1o  7214  domss2  7269  php3  7296  isinf  7325  ssfi  7332  oef1o  7658  cnfcomlem  7659  cnfcom  7660  cnfcom2  7662  cnfcom3  7664  cnfcom3clem  7665  infxpenc  7904  infxpenc2lem2  7906  infxpenc2  7908  ackbij2lem2  8125  ackbij2  8128  canthp1lem2  8533  pwfseqlem5  8543  pwfseq  8544  seqf1olem2  11368  seqf1o  11369  hasheqf1oi  11640  hashf1rn  11641  hashfacen  11708  summo  12516  fsum  12519  ackbijnn  12612  bitsf1ocnv  12961  sadcaddlem  12974  unbenlem  13281  setcinv  14250  yonffthlem  14384  grplactcnv  14892  eqgen  14998  isgim  15054  elsymgbas2  15101  cayleyth  15118  gsumval3eu  15518  gsumval3  15519  islmim  16139  coe1mul2lem2  16666  znunithash  16850  tgpconcompeqg  18146  resinf1o  20443  efif1olem4  20452  logf1o  20467  relogf1o  20469  dvlog  20547  nbgraf1o0  21461  cusgrafilem3  21495  iseupa  21692  eupares  21702  eupap1  21703  hoif  23262  indf1o  24426  derangenlem  24862  subfacp1lem2a  24871  subfacp1lem3  24873  subfacp1lem5  24875  subfacp1lem6  24876  subfacp1  24877  elgiso  25112  prodmo  25267  fprod  25272  isismty  26524  ismrer1  26561  isrngoiso  26608  eldioph2lem1  26832  enfixsn  27248  pwfi2f1o  27251  frgrancvvdeqlem9  28504  islaut  30954  ispautN  30970  hvmap1o  32635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464
  Copyright terms: Public domain W3C validator