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

Theorem f1oeq2 5464
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 5433 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5448 . . 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 5262 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5262 . 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 1623   -1-1->wf1 5252   -onto->wfo 5253   -1-1-onto->wf1o 5254
This theorem is referenced by:  f1oeq23  5466  f1oeq123d  5469  resin  5495  f1osng  5514  f1oprswap  5515  fveqf1o  5806  isoeq4  5819  oacomf1o  6563  bren  6871  marypha1lem  7186  oef1o  7401  cnfcomlem  7402  cnfcom  7403  cnfcom2  7405  infxpenc  7645  infxpenc2  7649  pwfseqlem5  8285  pwfseq  8286  summolem3  12187  summo  12190  fsum  12193  fsumf1o  12196  sumsn  12213  gsumvalx  14451  gsumpropd  14453  gsumval3  15191  znhash  16512  znunithash  16518  imasf1oxms  18035  cncfcnvcn  18424  gsumpropd2lem  23379  derangval  23698  subfacp1lem2a  23711  subfacp1lem3  23713  subfacp1lem5  23715  erdsze2lem1  23734  eupai  23883  eupa0  23898  eupares  23899  eupap1  23900  elgiso  24003  ismtyval  26524  rngoisoval  26608  eldioph2lem1  26839  imasgim  27264  sumsnd  27697  stoweidlem35  27784  stoweidlem39  27788  lautset  30271  pautsetN  30287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262
  Copyright terms: Public domain W3C validator