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

Theorem f1oeq1 5465
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 5434 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5449 . . 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 5264 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5264 . 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 1625   -1-1->wf1 5254   -onto->wfo 5255   -1-1-onto->wf1o 5256
This theorem is referenced by:  f1oeq123d  5471  f1ocnvb  5488  f1orescnv  5490  resin  5497  f1ovi  5514  f1osng  5516  f1oprswap  5517  fsn  5698  fveqf1o  5808  isoeq1  5818  oacomf1o  6565  mapsn  6811  mapsnf1o3  6818  f1oen3g  6879  ensn1  6927  xpcomf1o  6953  omf1o  6967  domss2  7022  php3  7049  isinf  7078  ssfi  7085  oef1o  7403  cnfcomlem  7404  cnfcom  7405  cnfcom2  7407  cnfcom3  7409  cnfcom3clem  7410  infxpenc  7647  infxpenc2lem2  7649  infxpenc2  7651  ackbij2lem2  7868  ackbij2  7871  canthp1lem2  8277  pwfseqlem5  8287  pwfseq  8288  seqf1olem2  11088  seqf1o  11089  hashfacen  11394  summo  12192  fsum  12195  ackbijnn  12288  bitsf1ocnv  12637  sadcaddlem  12650  unbenlem  12957  setcinv  13924  yonffthlem  14058  grplactcnv  14566  eqgen  14672  isgim  14728  elsymgbas2  14775  cayleyth  14792  gsumval3eu  15192  gsumval3  15193  islmim  15817  coe1mul2lem2  16347  znunithash  16520  tgpconcompeqg  17796  resinf1o  19900  efif1olem4  19909  logf1o  19924  relogf1o  19926  dvlog  20000  hoif  22336  indf1o  23609  derangenlem  23704  subfacp1lem2a  23713  subfacp1lem3  23715  subfacp1lem5  23717  subfacp1lem6  23718  subfacp1  23719  iseupa  23883  eupares  23901  eupap1  23902  elgiso  24005  cbicp  25177  isoriso2  25224  gapm2  25380  trooo  25405  ltrooo  25415  rltrooo  25426  isismty  26536  ismrer1  26573  isrngoiso  26620  eldioph2lem1  26850  enfixsn  27268  pwfi2f1o  27271  islaut  30345  ispautN  30361  hvmap1o  32026
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264
  Copyright terms: Public domain W3C validator