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

Theorem f1oeq2 5808
Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1oeq2  |-  ( A  =  B  ->  ( F : A -1-1-onto-> C  <->  F : B -1-1-onto-> C ) )

Proof of Theorem f1oeq2
StepHypRef Expression
1 f1eq2 5777 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5792 . . 3  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
31, 2anbi12d 710 . 2  |-  ( A  =  B  ->  (
( F : A -1-1-> C  /\  F : A -onto-> C )  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) ) )
4 df-f1o 5595 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5595 . 2  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
63, 4, 53bitr4g 288 1  |-  ( A  =  B  ->  ( F : A -1-1-onto-> C  <->  F : B -1-1-onto-> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   -1-1->wf1 5585   -onto->wfo 5586   -1-1-onto->wf1o 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595
This theorem is referenced by:  f1oeq23  5810  f1oeq123d  5813  resin  5837  f1osng  5854  f1o2sn  6065  fveqf1o  6194  isoeq4  6207  oacomf1o  7215  bren  7526  marypha1lem  7894  oef1o  8142  oef1oOLD  8143  cnfcomlem  8144  cnfcom  8145  cnfcom2  8147  cnfcomlemOLD  8152  cnfcomOLD  8153  cnfcom2OLD  8155  infxpenc  8396  infxpenc2  8400  infxpencOLD  8401  infxpenc2OLD  8404  pwfseqlem5  9042  pwfseq  9043  summolem3  13502  summo  13505  fsum  13508  fsumf1o  13511  sumsn  13529  gsumvalx  15827  gsumpropd  15829  gsumpropd2lem  15830  gsumval3OLD  16723  gsumval3lem1  16724  gsumval3  16726  znhash  18404  znunithash  18410  imasf1oxms  20819  cncfcnvcn  21252  wlknwwlknvbij  24513  clwwlkvbij  24574  eupai  24740  eupatrl  24741  eupa0  24747  eupares  24748  eupap1  24749  derangval  28362  subfacp1lem2a  28375  subfacp1lem3  28377  subfacp1lem5  28379  erdsze2lem1  28398  elgiso  28787  prodmolem3  28918  prodmo  28921  fprod  28926  fprodf1o  28931  prodsn  28945  ismtyval  30126  rngoisoval  30210  eldioph2lem1  30524  imasgim  30879  sumsnd  31206  stoweidlem35  31562  stoweidlem39  31566  f1dmvrnfibi  32006  lautset  35095  pautsetN  35111
  Copyright terms: Public domain W3C validator