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

Theorem foeq3 5729
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 2469 . . 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 5535 . 2  |-  ( F : C -onto-> A  <->  ( F  Fn  C  /\  ran  F  =  A ) )
4 df-fo 5535 . 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 1370   ran crn 4952    Fn wfn 5524   -onto->wfo 5527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fo 5535
This theorem is referenced by:  f1oeq3  5745  foeq123d  5748  resdif  5772  ffoss  6651  fidomdm  7707  fifo  7797  brwdom  7897  brwdom2  7903  canthwdom  7909  ixpiunwdom  7921  fin1a2lem7  8690  znnen  13617  divslem  14604  znzrhfo  18115  rncmp  19141  conima  19171  concn  19172  qtopcmplem  19422  qtoprest  19432  opidon2  23990  pjhfo  25288  dmct  26192  ivthALT  28701
  Copyright terms: Public domain W3C validator