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

Theorem foeq3 5613
Description: Equality theorem for onto functions. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
foeq3  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )

Proof of Theorem foeq3
StepHypRef Expression
1 eqeq2 2447 . . 3  |-  ( A  =  B  ->  ( ran  F  =  A  <->  ran  F  =  B ) )
21anbi2d 703 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  =  A )  <->  ( F  Fn  C  /\  ran  F  =  B ) ) )
3 df-fo 5419 . 2  |-  ( F : C -onto-> A  <->  ( F  Fn  C  /\  ran  F  =  A ) )
4 df-fo 5419 . 2  |-  ( F : C -onto-> B  <->  ( F  Fn  C  /\  ran  F  =  B ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   ran crn 4836    Fn wfn 5408   -onto->wfo 5411
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 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-fo 5419
This theorem is referenced by:  f1oeq3  5629  foeq123d  5632  resdif  5656  ffoss  6533  fidomdm  7585  fifo  7674  brwdom  7774  brwdom2  7780  canthwdom  7786  ixpiunwdom  7798  fin1a2lem7  8567  znnen  13487  divslem  14473  znzrhfo  17955  rncmp  18974  conima  19004  concn  19005  qtopcmplem  19255  qtoprest  19265  opidon2  23762  pjhfo  25060  dmct  25965  ivthALT  28483
  Copyright terms: Public domain W3C validator