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

Theorem f1oeq1 5632
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 5601 . . 3  |-  ( F  =  G  ->  ( F : A -1-1-> B  <->  G : A -1-1-> B ) )
2 foeq1 5616 . . 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 5428 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
5 df-f1o 5428 . 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 5418   -onto->wfo 5419   -1-1-onto->wf1o 5420
This theorem is referenced by:  f1oeq123d  5638  f1ocnvb  5655  f1orescnv  5657  resin  5664  f1ovi  5681  f1osng  5683  fsn  5873  fveqf1o  5996  isoeq1  6006  oacomf1o  6775  mapsn  7022  mapsnf1o3  7029  f1oen3g  7090  ensn1  7138  xpcomf1o  7164  omf1o  7178  domss2  7233  php3  7260  isinf  7289  ssfi  7296  oef1o  7619  cnfcomlem  7620  cnfcom  7621  cnfcom2  7623  cnfcom3  7625  cnfcom3clem  7626  infxpenc  7863  infxpenc2lem2  7865  infxpenc2  7867  ackbij2lem2  8084  ackbij2  8087  canthp1lem2  8492  pwfseqlem5  8502  pwfseq  8503  seqf1olem2  11326  seqf1o  11327  hasheqf1oi  11598  hashf1rn  11599  hashfacen  11666  summo  12474  fsum  12477  ackbijnn  12570  bitsf1ocnv  12919  sadcaddlem  12932  unbenlem  13239  setcinv  14208  yonffthlem  14342  grplactcnv  14850  eqgen  14956  isgim  15012  elsymgbas2  15059  cayleyth  15076  gsumval3eu  15476  gsumval3  15477  islmim  16097  coe1mul2lem2  16624  znunithash  16808  tgpconcompeqg  18102  resinf1o  20399  efif1olem4  20408  logf1o  20423  relogf1o  20425  dvlog  20503  nbgraf1o0  21417  cusgrafilem3  21451  iseupa  21648  eupares  21658  eupap1  21659  hoif  23218  indf1o  24382  derangenlem  24818  subfacp1lem2a  24827  subfacp1lem3  24829  subfacp1lem5  24831  subfacp1lem6  24832  subfacp1  24833  elgiso  25068  prodmo  25223  fprod  25228  isismty  26408  ismrer1  26445  isrngoiso  26492  eldioph2lem1  26716  enfixsn  27133  pwfi2f1o  27136  frgrancvvdeqlem9  28152  islaut  30577  ispautN  30593  hvmap1o  32258
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
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 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428
  Copyright terms: Public domain W3C validator