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

Theorem f1oeq1 5598
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 5567 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5582 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 692 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5394 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5394 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 280 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 177    /\ wa 359    = wceq 1649   -1-1->wf1 5384   -onto->wfo 5385   -1-1-onto->wf1o 5386
This theorem is referenced by:  f1oeq123d  5604  f1ocnvb  5621  f1orescnv  5623  resin  5630  f1ovi  5647  f1osng  5649  fsn  5838  fveqf1o  5961  isoeq1  5971  oacomf1o  6737  mapsn  6984  mapsnf1o3  6991  f1oen3g  7052  ensn1  7100  xpcomf1o  7126  omf1o  7140  domss2  7195  php3  7222  isinf  7251  ssfi  7258  oef1o  7581  cnfcomlem  7582  cnfcom  7583  cnfcom2  7585  cnfcom3  7587  cnfcom3clem  7588  infxpenc  7825  infxpenc2lem2  7827  infxpenc2  7829  ackbij2lem2  8046  ackbij2  8049  canthp1lem2  8454  pwfseqlem5  8464  pwfseq  8465  seqf1olem2  11283  seqf1o  11284  hasheqf1oi  11555  hashfacen  11623  summo  12431  fsum  12434  ackbijnn  12527  bitsf1ocnv  12876  sadcaddlem  12889  unbenlem  13196  setcinv  14165  yonffthlem  14299  grplactcnv  14807  eqgen  14913  isgim  14969  elsymgbas2  15016  cayleyth  15033  gsumval3eu  15433  gsumval3  15434  islmim  16054  coe1mul2lem2  16581  znunithash  16761  tgpconcompeqg  18055  resinf1o  20298  efif1olem4  20307  logf1o  20322  relogf1o  20324  dvlog  20402  nbgraf1o0  21315  cusgrafilem3  21349  iseupa  21528  eupares  21538  eupap1  21539  hoif  23098  indf1o  24210  derangenlem  24629  subfacp1lem2a  24638  subfacp1lem3  24640  subfacp1lem5  24642  subfacp1lem6  24643  subfacp1  24644  elgiso  24879  prodmo  25034  fprod  25039  isismty  26194  ismrer1  26231  isrngoiso  26278  eldioph2lem1  26502  enfixsn  26919  pwfi2f1o  26922  frgrancvvdeqlem9  27786  islaut  30248  ispautN  30264  hvmap1o  31929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-br 4147  df-opab 4201  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394
  Copyright terms: Public domain W3C validator