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

Theorem f1oeq2 5502
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 5471 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5486 . . 3  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
31, 2anbi12d 691 . 2  |-  ( A  =  B  ->  (
( F : A -1-1-> C  /\  F : A -onto-> C )  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) ) )
4 df-f1o 5299 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5299 . 2  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
63, 4, 53bitr4g 279 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 176    /\ wa 358    = wceq 1633   -1-1->wf1 5289   -onto->wfo 5290   -1-1-onto->wf1o 5291
This theorem is referenced by:  f1oeq23  5504  f1oeq123d  5507  resin  5533  f1osng  5552  f1oprswap  5553  fveqf1o  5848  isoeq4  5861  oacomf1o  6605  bren  6914  marypha1lem  7231  oef1o  7446  cnfcomlem  7447  cnfcom  7448  cnfcom2  7450  infxpenc  7690  infxpenc2  7694  pwfseqlem5  8330  pwfseq  8331  summolem3  12234  summo  12237  fsum  12240  fsumf1o  12243  sumsn  12260  gsumvalx  14500  gsumpropd  14502  gsumval3  15240  znhash  16568  znunithash  16574  imasf1oxms  18087  cncfcnvcn  18477  gsumpropd2lem  23357  derangval  23982  subfacp1lem2a  23995  subfacp1lem3  23997  subfacp1lem5  23999  erdsze2lem1  24018  eupai  24167  eupa0  24182  eupares  24183  eupap1  24184  elgiso  24287  prodmolem3  24436  prodmo  24439  fprod  24444  fprodf1o  24449  prodsn  24462  ismtyval  25672  rngoisoval  25756  eldioph2lem1  25987  imasgim  26412  sumsnd  26845  stoweidlem35  26932  stoweidlem39  26936  eupatrl  27523  lautset  30089  pautsetN  30105
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-cleq 2309  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299
  Copyright terms: Public domain W3C validator