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

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

Proof of Theorem foeq2
StepHypRef Expression
1 fneq2 5535 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 686 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  =  C )  <->  ( F  Fn  B  /\  ran  F  =  C ) ) )
3 df-fo 5460 . 2  |-  ( F : A -onto-> C  <->  ( F  Fn  A  /\  ran  F  =  C ) )
4 df-fo 5460 . 2  |-  ( F : B -onto-> C  <->  ( F  Fn  B  /\  ran  F  =  C ) )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652   ran crn 4879    Fn wfn 5449   -onto->wfo 5452
This theorem is referenced by:  f1oeq2  5666  foeq123d  5670  tposfo  6506  brwdom  7535  brwdom2  7541  canthwdom  7547  cfslb2n  8148  fodomg  8403  0ramcl  13391  ghmcyg  15505  txcmpb  17676  qtoptopon  17736  opidon2  21912
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429  df-fn 5457  df-fo 5460
  Copyright terms: Public domain W3C validator