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

Theorem feq2d 5333
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 5329 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1348  wf 5192
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5199  df-f 5200
This theorem is referenced by:  feq12d  5335  ffdm  5366  fsng  5667  issmo2  6266  qliftf  6596  elpm2r  6642  casef  7063  fseq1p1m1  10043  fseq1m1p1  10044  seqf  10410  seqf2  10413  intopsn  12614  lmtopcnp  13009  ellimc3apf  13388  dvidlemap  13419  dviaddf  13428  dvimulf  13429  dvcjbr  13431  dvcj  13432  dvrecap  13436  dvmptclx  13439
  Copyright terms: Public domain W3C validator