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

Theorem foeq3 5610
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 2413 . . 3  |-  ( A  =  B  ->  ( ran  F  =  A  <->  ran  F  =  B ) )
21anbi2d 685 . 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 280 1  |-  ( A  =  B  ->  ( F : C -onto-> A  <->  F : C -onto-> B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649   ran crn 4838    Fn wfn 5408   -onto->wfo 5411
This theorem is referenced by:  f1oeq3  5626  foeq123d  5629  resdif  5655  ffoss  5666  fidomdm  7347  fifo  7395  brwdom  7491  brwdom2  7497  canthwdom  7503  ixpiunwdom  7515  fin1a2lem7  8242  znnen  12767  divslem  13723  znzrhfo  16783  rncmp  17413  conima  17441  concn  17442  qtopcmplem  17692  qtoprest  17702  opidon2  21865  pjhfo  23161  dmct  24059  ivthALT  26228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-fo 5419
  Copyright terms: Public domain W3C validator