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

Theorem f1oeq2 5654
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 5623 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5638 . . 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 5446 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5446 . 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 1369   -1-1->wf1 5436   -onto->wfo 5437   -1-1-onto->wf1o 5438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446
This theorem is referenced by:  f1oeq23  5656  f1oeq123d  5659  resin  5683  f1osng  5700  fveqf1o  6021  isoeq4  6034  oacomf1o  7025  bren  7340  marypha1lem  7704  oef1o  7951  oef1oOLD  7952  cnfcomlem  7953  cnfcom  7954  cnfcom2  7956  cnfcomlemOLD  7961  cnfcomOLD  7962  cnfcom2OLD  7964  infxpenc  8205  infxpenc2  8209  infxpencOLD  8210  infxpenc2OLD  8213  pwfseqlem5  8851  pwfseq  8852  summolem3  13212  summo  13215  fsum  13218  fsumf1o  13221  sumsn  13238  gsumvalx  15523  gsumpropd  15525  gsumpropd2lem  15526  gsumval3OLD  16403  gsumval3lem1  16404  gsumval3  16406  znhash  18013  znunithash  18019  imasf1oxms  20086  cncfcnvcn  20519  eupai  23610  eupatrl  23611  eupa0  23617  eupares  23618  eupap1  23619  derangval  27077  subfacp1lem2a  27090  subfacp1lem3  27092  subfacp1lem5  27094  erdsze2lem1  27113  elgiso  27337  prodmolem3  27468  prodmo  27471  fprod  27476  fprodf1o  27481  prodsn  27495  ismtyval  28725  rngoisoval  28809  eldioph2lem1  29124  imasgim  29481  sumsnd  29774  stoweidlem35  29856  stoweidlem39  29860  wlknwwlknvbij  30398  clwwlkvbij  30489  f1o2sn  30752  lautset  33822  pautsetN  33838
  Copyright terms: Public domain W3C validator