Theorem fneq2d 6417

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

Step	Hyp	Ref	Expression
1		fneq2d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		fneq2 6415	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   Fn wfn 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fn 6327

This theorem is referenced by:  fneq12d  6418  fnprb  6948  fntpb  6949  fnpr2g  6950  undifixp  8481  brwdom2  9021  dfac3  9532  ac7g  9885  ccatlid  13931  ccatrid  13932  ccatass  13933  ccatswrd  14021  swrdccat2  14022  ccatpfx  14054  swrdswrd  14058  swrdccatin2  14082  pfxccatin12  14086  revccat  14119  revrev  14120  repsdf2  14131  0csh0  14146  cshco  14189  wrd2pr2op  14296  wrd3tpop  14301  ofccat  14320  seqshft  14436  invf  17030  sscfn1  17079  sscfn2  17080  isssc  17082  fuchom  17223  estrchomfeqhom  17378  mulgfval  18218  mulgfvalALT  18219  frlmsslss2  20464  subrgascl  20737  m1detdiag  21202  ptval  22175  xpsdsfn2  22985  fresf1o  30390  psgndmfi  30790  cycpmconjslem1  30846  cycpmconjslem2  30847  pl1cn  31308  signsvtn0  31950  signstres  31955  bnj927  32150  revpfxsfxrev  32475  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  dibfnN  38452  dihintcl  38640  frlmvscadiccat  39440  uzmptshftfval  41050  srhmsubc  44700  srhmsubcALTV  44718