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

Theorem feq2d 5354
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 5350 . 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 105    = wceq 1353   -->wf 5213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5220  df-f 5221
This theorem is referenced by:  feq12d  5356  ffdm  5387  fsng  5690  issmo2  6290  qliftf  6620  elpm2r  6666  casef  7087  fseq1p1m1  10094  fseq1m1p1  10095  seqf  10461  seqf2  10464  intopsn  12786  lmtopcnp  13753  ellimc3apf  14132  dvidlemap  14163  dviaddf  14172  dvimulf  14173  dvcjbr  14175  dvcj  14176  dvrecap  14180  dvmptclx  14183
  Copyright terms: Public domain W3C validator