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

Theorem f1oeq2 5804
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 5773 . . 3  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
2 foeq2 5788 . . 3  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
31, 2anbi12d 716 . 2  |-  ( A  =  B  ->  (
( F : A -1-1-> C  /\  F : A -onto-> C )  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) ) )
4 df-f1o 5588 . 2  |-  ( F : A -1-1-onto-> C  <->  ( F : A -1-1-> C  /\  F : A -onto-> C ) )
5 df-f1o 5588 . 2  |-  ( F : B -1-1-onto-> C  <->  ( F : B -1-1-> C  /\  F : B -onto-> C ) )
63, 4, 53bitr4g 292 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 188    /\ wa 371    = wceq 1443   -1-1->wf1 5578   -onto->wfo 5579   -1-1-onto->wf1o 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-cleq 2443  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588
This theorem is referenced by:  f1oeq23  5806  f1oeq123d  5809  resin  5833  f1osng  5851  f1o2sn  6065  fveqf1o  6198  isoeq4  6211  oacomf1o  7263  bren  7575  f1dmvrnfibi  7855  marypha1lem  7944  oef1o  8200  cnfcomlem  8201  cnfcom  8202  cnfcom2  8204  infxpenc  8446  infxpenc2  8450  pwfseqlem5  9085  pwfseq  9086  summolem3  13773  summo  13776  fsum  13779  fsumf1o  13782  sumsn  13800  prodmolem3  13980  prodmo  13983  fprod  13988  fprodf1o  13993  prodsn  14009  prodsnf  14011  gsumvalx  16506  gsumpropd  16508  gsumpropd2lem  16509  gsumval3lem1  17532  gsumval3  17534  znhash  19122  znunithash  19128  imasf1oxms  21497  cncfcnvcn  21946  wlknwwlknvbij  25461  clwwlkvbij  25522  eupai  25688  eupatrl  25689  eupa0  25695  eupares  25696  eupap1  25697  f1ocnt  28369  derangval  29883  subfacp1lem2a  29896  subfacp1lem3  29898  subfacp1lem5  29900  erdsze2lem1  29919  elgiso  30307  ismtyval  32125  rngoisoval  32209  lautset  33641  pautsetN  33657  eldioph2lem1  35596  imasgim  35952  sumsnd  37341  f1oeq2d  37441  sumsnf  37642  stoweidlem35  37890  stoweidlem39  37894
  Copyright terms: Public domain W3C validator