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

Theorem foeq3 5804
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 2437 . . 3  |-  ( A  =  B  ->  ( ran  F  =  A  <->  ran  F  =  B ) )
21anbi2d 708 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  =  A )  <->  ( F  Fn  C  /\  ran  F  =  B ) ) )
3 df-fo 5603 . 2  |-  ( F : C -onto-> A  <->  ( F  Fn  C  /\  ran  F  =  A ) )
4 df-fo 5603 . 2  |-  ( F : C -onto-> B  <->  ( F  Fn  C  /\  ran  F  =  B ) )
52, 3, 43bitr4g 291 1  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   ran crn 4850    Fn wfn 5592   -onto->wfo 5595
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 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414  df-fo 5603
This theorem is referenced by:  f1oeq3  5820  foeq123d  5823  resdif  5847  ffoss  6764  fidomdm  7855  fifo  7948  brwdom  8084  brwdom2  8090  canthwdom  8096  ixpiunwdom  8108  fin1a2lem7  8836  znnen  14252  quslem  15436  znzrhfo  19104  rncmp  20397  conima  20426  concn  20427  qtopcmplem  20708  qtoprest  20718  opidon2OLD  26037  pjhfo  27344  dmct  28291  msrfo  30179  ivthALT  30983  poimirlem26  31879  poimirlem27  31880  founiiun0  37314
  Copyright terms: Public domain W3C validator