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

Theorem f1oeq1 5797
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 5766 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5781 . . 3  |-  ( F  =  G  ->  ( F : A -onto-> B  <->  G : A -onto-> B ) )
31, 2anbi12d 710 . 2  |-  ( F  =  G  ->  (
( F : A -1-1-> B  /\  F : A -onto-> B )  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) ) )
4 df-f1o 5585 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5585 . 2  |-  ( G : A -1-1-onto-> B  <->  ( G : A -1-1-> B  /\  G : A -onto-> B ) )
63, 4, 53bitr4g 288 1  |-  ( F  =  G  ->  ( F : A -1-1-onto-> B  <->  G : A -1-1-onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383   -1-1->wf1 5575   -onto->wfo 5576   -1-1-onto->wf1o 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-br 4438  df-opab 4496  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585
This theorem is referenced by:  f1oeq123d  5803  f1ocnvb  5819  f1orescnv  5821  resin  5827  f1ovi  5842  f1osng  5844  f1oresrab  6048  fsn  6054  fveqf1o  6190  isoeq1  6200  f1oexbi  6735  oacomf1o  7216  mapsn  7462  mapsnf1o3  7469  f1oen3g  7533  ensn1  7581  xpcomf1o  7608  omf1o  7622  enfixsn  7628  domss2  7678  php3  7705  isinf  7735  ssfi  7742  oef1o  8144  oef1oOLD  8145  cnfcomlem  8146  cnfcom  8147  cnfcom2  8149  cnfcom3  8151  cnfcom3clem  8152  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom2OLD  8157  cnfcom3OLD  8159  cnfcom3clemOLD  8160  infxpenc  8398  infxpenc2lem2  8400  infxpenc2  8402  infxpencOLD  8403  infxpenc2lem2OLD  8404  infxpenc2OLD  8406  ackbij2lem2  8623  ackbij2  8626  canthp1lem2  9034  pwfseqlem5  9044  pwfseq  9045  seqf1olem2  12129  seqf1o  12130  hasheqf1oi  12406  hashf1rn  12407  hashfacen  12485  wrd2f1tovbij  12880  summo  13521  fsum  13524  ackbijnn  13622  prodmo  13725  fprod  13730  bitsf1ocnv  14076  sadcaddlem  14089  unbenlem  14408  setcinv  15396  yonffthlem  15530  grplactcnv  16117  eqgen  16233  isgim  16289  elsymgbas2  16385  symg1bas  16400  cayleyth  16419  gsumval3eu  16886  gsumval3OLD  16887  gsumval3lem1  16888  gsumval3lem2  16889  islmim  17687  coe1mul2lem2  18288  znunithash  18581  uvcendim  18860  mdet0f1o  19073  tgpconcompeqg  20588  resinf1o  22901  efif1olem4  22910  logf1o  22930  relogf1o  22932  dvlog  23010  isismt  23899  nbgraf1o0  24424  cusgrafilem3  24459  wlknwwlknbij2  24692  wlkiswwlkbij2  24699  wwlkextbij  24711  wlknwwlknvbij  24718  clwwlkbij  24777  clwwlkvbij  24779  clwlksizeeq  24830  iseupa  24943  eupares  24953  eupap1  24954  frgrancvvdeqlem9  25019  numclwlk1lem2  25075  numclwwlk2lem3  25084  hoif  26651  rabfodom  27382  fcobijfs  27527  fpwrelmapffs  27535  indf1o  28015  eulerpartlem1  28284  eulerpartgbij  28289  eulerpart  28299  derangenlem  28593  subfacp1lem2a  28602  subfacp1lem3  28604  subfacp1lem5  28606  subfacp1lem6  28607  subfacp1  28608  elgiso  29014  isismty  30273  ismrer1  30310  isrngoiso  30357  eldioph2lem1  30669  pwfi2f1o  31020  equivestrcsetc  32624  islaut  35682  ispautN  35698  hvmap1o  37365
  Copyright terms: Public domain W3C validator