MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fneq2d Structured version   Visualization version   GIF version

Theorem fneq2d 6440
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
fneq2d (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))

Proof of Theorem fneq2d
StepHypRef Expression
1 fneq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 fneq2 6438 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1530   Fn wfn 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812  df-fn 6351
This theorem is referenced by:  fneq12d  6441  fnprb  6963  fntpb  6964  fnpr2g  6965  undifixp  8490  brwdom2  9029  dfac3  9539  ac7g  9888  ccatlid  13932  ccatrid  13933  ccatass  13934  ccatswrd  14022  swrdccat2  14023  ccatpfx  14055  swrdswrd  14059  swrdccatin2  14083  pfxccatin12  14087  revccat  14120  revrev  14121  repsdf2  14132  0csh0  14147  cshco  14190  wrd2pr2op  14297  wrd3tpop  14302  ofccat  14321  seqshft  14436  invf  17030  sscfn1  17079  sscfn2  17080  isssc  17082  fuchom  17223  estrchomfeqhom  17378  mulgfval  18218  mulgfvalALT  18219  subrgascl  20270  frlmsslss2  20911  m1detdiag  21198  ptval  22170  xpsdsfn2  22980  fresf1o  30368  psgndmfi  30733  cycpmconjslem1  30789  cycpmconjslem2  30790  pl1cn  31186  signsvtn0  31828  signstres  31833  bnj927  32028  revpfxsfxrev  32350  poimirlem1  34880  poimirlem2  34881  poimirlem3  34882  poimirlem4  34883  poimirlem6  34885  poimirlem7  34886  poimirlem11  34890  poimirlem12  34891  poimirlem16  34895  poimirlem17  34896  poimirlem19  34898  poimirlem20  34899  dibfnN  38279  dihintcl  38467  frlmvscadiccat  39130  uzmptshftfval  40663  srhmsubc  44332  srhmsubcALTV  44350
  Copyright terms: Public domain W3C validator