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

Theorem foeq2 5486
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 5371 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 685 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  =  C )  <->  ( F  Fn  B  /\  ran  F  =  C ) ) )
3 df-fo 5298 . 2  |-  ( F : A -onto-> C  <->  ( F  Fn  A  /\  ran  F  =  C ) )
4 df-fo 5298 . 2  |-  ( F : B -onto-> C  <->  ( F  Fn  B  /\  ran  F  =  C ) )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( F : A -onto-> C  <->  F : B -onto-> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1633   ran crn 4727    Fn wfn 5287   -onto->wfo 5290
This theorem is referenced by:  f1oeq2  5502  foeq123d  5506  tposfo  6303  brwdom  7326  brwdom2  7332  canthwdom  7338  cfslb2n  7939  fodomg  8195  0ramcl  13117  ghmcyg  15231  txcmpb  17394  qtoptopon  17451  opidon2  21044
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-cleq 2309  df-fn 5295  df-fo 5298
  Copyright terms: Public domain W3C validator