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

Theorem feq2d 5269
 Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
feq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
feq2d (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))

Proof of Theorem feq2d
StepHypRef Expression
1 feq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 feq2 5265 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332  ⟶wf 5128 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-fn 5135  df-f 5136 This theorem is referenced by:  feq12d  5271  ffdm  5302  fsng  5602  issmo2  6195  qliftf  6523  elpm2r  6569  casef  6983  fseq1p1m1  9925  fseq1m1p1  9926  seqf  10285  seqf2  10288  lmtopcnp  12478  ellimc3apf  12857  dvidlemap  12888  dviaddf  12897  dvimulf  12898  dvcjbr  12900  dvcj  12901  dvrecap  12905  dvmptclx  12908
 Copyright terms: Public domain W3C validator