ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  feq2 Unicode version

Theorem feq2 5082
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 5039 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 453 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 4956 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 4956 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 221 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285    C_ wss 2982   ran crn 4392    Fn wfn 4947   -->wf 4948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-fn 4955  df-f 4956
This theorem is referenced by:  feq23  5084  feq2d  5086  feq2i  5091  f00  5132  f1eq2  5139  fressnfv  5402  tfrcllemsucfn  6022  tfrcllemsucaccv  6023  tfrcllembxssdm  6025  tfrcllembfn  6026  tfrcllemaccex  6030  tfrcllemres  6031  tfrcldm  6032  tfrcl  6033  ac6sfi  6454
  Copyright terms: Public domain W3C validator