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

Theorem foeq3 5814
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 2473 . . 3  |-  ( A  =  B  ->  ( ran  F  =  A  <->  ran  F  =  B ) )
21anbi2d 715 . 2  |-  ( A  =  B  ->  (
( F  Fn  C  /\  ran  F  =  A )  <->  ( F  Fn  C  /\  ran  F  =  B ) ) )
3 df-fo 5607 . 2  |-  ( F : C -onto-> A  <->  ( F  Fn  C  /\  ran  F  =  A ) )
4 df-fo 5607 . 2  |-  ( F : C -onto-> B  <->  ( F  Fn  C  /\  ran  F  =  B ) )
52, 3, 43bitr4g 296 1  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1455   ran crn 4854    Fn wfn 5596   -onto->wfo 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-cleq 2455  df-fo 5607
This theorem is referenced by:  f1oeq3  5830  foeq123d  5833  resdif  5857  ffoss  6781  fidomdm  7879  fifo  7972  brwdom  8108  brwdom2  8114  canthwdom  8120  ixpiunwdom  8132  fin1a2lem7  8862  znnen  14314  quslem  15498  znzrhfo  19167  rncmp  20460  conima  20489  concn  20490  qtopcmplem  20771  qtoprest  20781  opidon2OLD  26101  pjhfo  27408  dmct  28347  msrfo  30233  ivthALT  31040  poimirlem26  32011  poimirlem27  32012  founiiun0  37503
  Copyright terms: Public domain W3C validator