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

Theorem f1oeq2 5668
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 5637 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5652 . . 3  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
31, 2anbi12d 693 . 2  |-  ( A  =  B  ->  (
( F : A -1-1-> C  /\  F : A -onto-> C )  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) ) )
4 df-f1o 5463 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5463 . 2  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
63, 4, 53bitr4g 281 1  |-  ( A  =  B  ->  ( F : A -1-1-onto-> C  <->  F : B -1-1-onto-> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   -1-1->wf1 5453   -onto->wfo 5454   -1-1-onto->wf1o 5455
This theorem is referenced by:  f1oeq23  5670  f1oeq123d  5673  resin  5699  f1osng  5718  fveqf1o  6031  isoeq4  6044  oacomf1o  6810  bren  7119  marypha1lem  7440  oef1o  7657  cnfcomlem  7658  cnfcom  7659  cnfcom2  7661  infxpenc  7901  infxpenc2  7905  pwfseqlem5  8540  pwfseq  8541  summolem3  12510  summo  12513  fsum  12516  fsumf1o  12519  sumsn  12536  gsumvalx  14776  gsumpropd  14778  gsumval3  15516  znhash  16841  znunithash  16847  imasf1oxms  18521  cncfcnvcn  18953  eupai  21691  eupatrl  21692  eupa0  21698  eupares  21699  eupap1  21700  gsumpropd2lem  24222  derangval  24855  subfacp1lem2a  24868  subfacp1lem3  24870  subfacp1lem5  24872  erdsze2lem1  24891  elgiso  25109  prodmolem3  25261  prodmo  25264  fprod  25269  fprodf1o  25274  prodsn  25288  ismtyval  26511  rngoisoval  26595  eldioph2lem1  26820  imasgim  27243  sumsnd  27675  stoweidlem35  27762  stoweidlem39  27766  lautset  30941  pautsetN  30957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463
  Copyright terms: Public domain W3C validator