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

Theorem feq2d 5260
Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
feq2d  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 feq2 5256 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2syl 14 1  |-  ( ph  ->  ( F : A --> C 
<->  F : B --> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1331   -->wf 5119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-fn 5126  df-f 5127
This theorem is referenced by:  feq12d  5262  ffdm  5293  fsng  5593  issmo2  6186  qliftf  6514  elpm2r  6560  casef  6973  fseq1p1m1  9874  fseq1m1p1  9875  seqf  10234  seqf2  10237  lmtopcnp  12419  ellimc3apf  12798  dvidlemap  12829  dviaddf  12838  dvimulf  12839  dvcjbr  12841  dvcj  12842  dvrecap  12846  dvmptclx  12849
  Copyright terms: Public domain W3C validator