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

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

Proof of Theorem feq2
StepHypRef Expression
1 fneq2 5439 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 685 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5362 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5362 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1647    C_ wss 3238   ran crn 4793    Fn wfn 5353   -->wf 5354
This theorem is referenced by:  feq23  5483  feq2d  5485  feq2i  5490  f00  5532  f1eq2  5539  fressnfv  5820  fconstfv  5854  mapvalg  6925  map0g  6950  ac6sfi  7248  cofsmo  8042  axcc4dom  8214  ac6sg  8262  isghm  14893  pjdm2  16828  cmpcovf  17335  ulmval  19974  measval  24138  isrnmeas  24140  poseq  25079  soseq  25080  elno2  25134  noreson  25140  noxpsgn  25145  nodenselem6  25166  stoweidlem62  27402
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-cleq 2359  df-fn 5361  df-f 5362
  Copyright terms: Public domain W3C validator