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

Theorem f1oeq2 5814
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 5783 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5798 . . 3  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
31, 2anbi12d 715 . 2  |-  ( A  =  B  ->  (
( F : A -1-1-> C  /\  F : A -onto-> C )  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) ) )
4 df-f1o 5599 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5599 . 2  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
63, 4, 53bitr4g 291 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 187    /\ wa 370    = wceq 1437   -1-1->wf1 5589   -onto->wfo 5590   -1-1-onto->wf1o 5591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2412  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599
This theorem is referenced by:  f1oeq23  5816  f1oeq123d  5819  resin  5843  f1osng  5860  f1o2sn  6073  fveqf1o  6206  isoeq4  6219  oacomf1o  7265  bren  7577  f1dmvrnfibi  7855  marypha1lem  7944  oef1o  8193  cnfcomlem  8194  cnfcom  8195  cnfcom2  8197  infxpenc  8438  infxpenc2  8442  pwfseqlem5  9077  pwfseq  9078  summolem3  13747  summo  13750  fsum  13753  fsumf1o  13756  sumsn  13774  prodmolem3  13954  prodmo  13957  fprod  13962  fprodf1o  13967  prodsn  13983  prodsnf  13985  gsumvalx  16465  gsumpropd  16467  gsumpropd2lem  16468  gsumval3lem1  17480  gsumval3  17482  znhash  19066  znunithash  19072  imasf1oxms  21441  cncfcnvcn  21875  wlknwwlknvbij  25354  clwwlkvbij  25415  eupai  25581  eupatrl  25582  eupa0  25588  eupares  25589  eupap1  25590  f1ocnt  28253  derangval  29719  subfacp1lem2a  29732  subfacp1lem3  29734  subfacp1lem5  29736  erdsze2lem1  29755  elgiso  30143  ismtyval  31880  rngoisoval  31964  lautset  33400  pautsetN  33416  eldioph2lem1  35355  imasgim  35712  sumsnd  37035  f1oeq2d  37118  sumsnf  37271  stoweidlem35  37513  stoweidlem39  37517
  Copyright terms: Public domain W3C validator