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

Theorem feq2 5544
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 5502 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 686 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5425 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5425 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 280 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3288   ran crn 4846    Fn wfn 5416   -->wf 5417
This theorem is referenced by:  feq23  5546  feq2d  5548  feq2i  5553  f00  5595  f1eq2  5602  fressnfv  5887  fconstfv  5921  mapvalg  6995  map0g  7020  ac6sfi  7318  cofsmo  8113  axcc4dom  8285  ac6sg  8332  isghm  14969  pjdm2  16901  cmpcovf  17416  ulmval  20257  measval  24513  isrnmeas  24515  poseq  25475  soseq  25476  elno2  25530  noreson  25536  noxpsgn  25541  nodenselem6  25562  mbfresfi  26160  stoweidlem62  27686
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 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2405  df-fn 5424  df-f 5425
  Copyright terms: Public domain W3C validator