Theorem fneq2d 6586

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 6584	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495

This theorem is referenced by:  fneq12d  6587  fncofn  6609  fnco  6610  fnprb  7154  fntpb  7155  fnpr2g  7156  undifixp  8872  brwdom2  9478  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  dfac3  10031  ac7g  10384  ccatlid  14510  ccatrid  14511  ccatass  14512  ccatswrd  14592  swrdccat2  14593  ccatpfx  14624  swrdswrd  14628  swrdccatin2  14652  pfxccatin12  14656  revccat  14689  revrev  14690  repsdf2  14701  0csh0  14716  cshco  14759  wrd2pr2op  14866  wrd3tpop  14871  ofccat  14892  seqshft  15008  invf  17692  sscfn1  17741  sscfn2  17742  isssc  17744  fuchom  17888  estrchomfeqhom  18059  mulgfval  18999  mulgfvalALT  19000  srhmsubc  20613  frlmsslss2  21730  subrgascl  22021  m1detdiag  22541  ptval  23514  xpsdsfn2  24322  fresf1o  32709  psgndmfi  33180  cycpmconjslem1  33236  cycpmconjslem2  33237  ply1annidllem  33858  pl1cn  34112  signsvtn0  34727  signstres  34732  bnj927  34925  fineqvac  35272  revpfxsfxrev  35310  ixpeq12dv  36410  cbvixpdavw  36472  cbvixpdavw2  36488  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  dibfnN  41416  dihintcl  41604  frlmvscadiccat  42761  selvvvval  42828  ofoafg  43596  uzmptshftfval  44587  srhmsubcALTV  48571  tposideq  49133  nelsubc3lem  49315  0funcg2  49329  fucofulem2  49556  termcfuncval  49777  termcnatval  49780  0fucterm  49788  cnelsubclem  49848