Theorem fneq2d 6601

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   Fn wfn 6496

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-fn 6504

This theorem is referenced by:  fneq12d  6602  fncofn  6622  fnco  6623  fnprb  7163  fntpb  7164  fnpr2g  7165  undifixp  8879  brwdom2  9518  brttrcl2  9659  ssttrcl  9660  ttrcltr  9661  ttrclss  9665  ttrclselem2  9671  dfac3  10066  ac7g  10419  ccatlid  14486  ccatrid  14487  ccatass  14488  ccatswrd  14568  swrdccat2  14569  ccatpfx  14601  swrdswrd  14605  swrdccatin2  14629  pfxccatin12  14633  revccat  14666  revrev  14667  repsdf2  14678  0csh0  14693  cshco  14737  wrd2pr2op  14844  wrd3tpop  14849  ofccat  14866  seqshft  14982  invf  17665  sscfn1  17714  sscfn2  17715  isssc  17717  fuchom  17863  fuchomOLD  17864  estrchomfeqhom  18037  mulgfval  18888  mulgfvalALT  18889  frlmsslss2  21218  subrgascl  21511  m1detdiag  21983  ptval  22958  xpsdsfn2  23768  fresf1o  31612  psgndmfi  32017  cycpmconjslem1  32073  cycpmconjslem2  32074  ply1annidllem  32458  pl1cn  32625  signsvtn0  33271  signstres  33276  bnj927  33470  fineqvac  33787  revpfxsfxrev  33796  poimirlem1  36152  poimirlem2  36153  poimirlem3  36154  poimirlem4  36155  poimirlem6  36157  poimirlem7  36158  poimirlem11  36162  poimirlem12  36163  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  dibfnN  39692  dihintcl  39880  frlmvscadiccat  40749  ofoafg  41747  uzmptshftfval  42748  srhmsubc  46494  srhmsubcALTV  46512