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

Theorem f1oeq1 5630
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 5599 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5614 . . 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 5423 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5423 . 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 1369   -1-1->wf1 5413   -onto->wfo 5414   -1-1-onto->wf1o 5415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-br 4291  df-opab 4349  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423
This theorem is referenced by:  f1oeq123d  5636  f1ocnvb  5652  f1orescnv  5654  resin  5660  f1ovi  5675  f1osng  5677  f1oresrab  5873  fsn  5879  fveqf1o  5998  isoeq1  6008  oacomf1o  7002  mapsn  7252  mapsnf1o3  7259  f1oen3g  7323  ensn1  7371  xpcomf1o  7398  omf1o  7412  enfixsn  7418  domss2  7468  php3  7495  isinf  7524  ssfi  7531  oef1o  7928  oef1oOLD  7929  cnfcomlem  7930  cnfcom  7931  cnfcom2  7933  cnfcom3  7935  cnfcom3clem  7936  cnfcomlemOLD  7938  cnfcomOLD  7939  cnfcom2OLD  7941  cnfcom3OLD  7943  cnfcom3clemOLD  7944  infxpenc  8182  infxpenc2lem2  8184  infxpenc2  8186  infxpencOLD  8187  infxpenc2lem2OLD  8188  infxpenc2OLD  8190  ackbij2lem2  8407  ackbij2  8410  canthp1lem2  8818  pwfseqlem5  8828  pwfseq  8829  seqf1olem2  11844  seqf1o  11845  hasheqf1oi  12120  hashf1rn  12121  hashfacen  12205  summo  13192  fsum  13195  ackbijnn  13289  bitsf1ocnv  13638  sadcaddlem  13651  unbenlem  13967  setcinv  14956  yonffthlem  15090  grplactcnv  15622  eqgen  15732  isgim  15788  elsymgbas2  15884  symg1bas  15899  cayleyth  15918  gsumval3eu  16379  gsumval3OLD  16380  gsumval3lem1  16381  gsumval3lem2  16382  islmim  17141  coe1mul2lem2  17720  znunithash  17995  uvcendim  18274  mdet0f1o  18402  tgpconcompeqg  19680  resinf1o  21990  efif1olem4  21999  logf1o  22014  relogf1o  22016  dvlog  22094  nbgraf1o0  23353  cusgrafilem3  23387  iseupa  23584  eupares  23594  eupap1  23595  hoif  25156  fcobijfs  26024  fpwrelmapffs  26032  indf1o  26478  eulerpartlem1  26748  eulerpartgbij  26753  eulerpart  26763  derangenlem  27057  subfacp1lem2a  27066  subfacp1lem3  27068  subfacp1lem5  27070  subfacp1lem6  27071  subfacp1  27072  elgiso  27313  prodmo  27447  fprod  27452  isismty  28697  ismrer1  28734  isrngoiso  28781  eldioph2lem1  29095  pwfi2f1o  29448  f1oexbi  30153  wrd2f1tovbij  30252  wlknwwlknbij2  30343  wlkiswwlkbij2  30350  wwlkextbij  30362  wlknwwlknvbij  30369  clwwlkbij  30458  clwwlkvbij  30460  clwlksizeeq  30522  frgrancvvdeqlem9  30631  numclwlk1lem2  30687  numclwwlk2lem3  30696  islaut  33724  ispautN  33740  hvmap1o  35405
  Copyright terms: Public domain W3C validator