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

Theorem feq2 5214
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 5170 . . 3  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
21anbi1d 458 . 2  |-  ( A  =  B  ->  (
( F  Fn  A  /\  ran  F  C_  C
)  <->  ( F  Fn  B  /\  ran  F  C_  C ) ) )
3 df-f 5085 . 2  |-  ( F : A --> C  <->  ( F  Fn  A  /\  ran  F  C_  C ) )
4 df-f 5085 . 2  |-  ( F : B --> C  <->  ( F  Fn  B  /\  ran  F  C_  C ) )
52, 3, 43bitr4g 222 1  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    = wceq 1314    C_ wss 3037   ran crn 4500    Fn wfn 5076   -->wf 5077
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-fn 5084  df-f 5085
This theorem is referenced by:  feq23  5216  feq2d  5218  feq2i  5224  f00  5272  f0dom0  5274  f1eq2  5282  fressnfv  5561  tfrcllemsucfn  6204  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllembfn  6208  tfrcllemaccex  6212  tfrcllemres  6213  tfrcldm  6214  tfrcl  6215  mapvalg  6506  map0g  6536  ac6sfi  6745  isomni  6958  ismkv  6977
  Copyright terms: Public domain W3C validator