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

Theorem feq2d 5216
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 5212 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2syl 14 1 (𝜑 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1312  wf 5075
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 1404  ax-gen 1406  ax-4 1468  ax-17 1487  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-fn 5082  df-f 5083
This theorem is referenced by:  feq12d  5218  ffdm  5249  fsng  5545  issmo2  6138  qliftf  6466  elpm2r  6512  casef  6923  fseq1p1m1  9761  fseq1m1p1  9762  seqf  10121  seqf2  10124  lmtopcnp  12255  ellimc3apf  12579  dvidlemap  12609  dviaddf  12616
  Copyright terms: Public domain W3C validator