Theorem fneq2d 6673

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576

This theorem is referenced by:  fneq12d  6674  fncofn  6696  fnco  6697  fnprb  7245  fntpb  7246  fnpr2g  7247  undifixp  8992  brwdom2  9642  brttrcl2  9783  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  dfac3  10190  ac7g  10543  ccatlid  14634  ccatrid  14635  ccatass  14636  ccatswrd  14716  swrdccat2  14717  ccatpfx  14749  swrdswrd  14753  swrdccatin2  14777  pfxccatin12  14781  revccat  14814  revrev  14815  repsdf2  14826  0csh0  14841  cshco  14885  wrd2pr2op  14992  wrd3tpop  14997  ofccat  15018  seqshft  15134  invf  17829  sscfn1  17878  sscfn2  17879  isssc  17881  fuchom  18030  fuchomOLD  18031  estrchomfeqhom  18204  mulgfval  19109  mulgfvalALT  19110  srhmsubc  20702  frlmsslss2  21818  subrgascl  22113  m1detdiag  22624  ptval  23599  xpsdsfn2  24409  fresf1o  32650  psgndmfi  33091  cycpmconjslem1  33147  cycpmconjslem2  33148  ply1annidllem  33694  pl1cn  33901  signsvtn0  34547  signstres  34552  bnj927  34745  fineqvac  35073  revpfxsfxrev  35083  ixpeq12dv  36182  cbvixpdavw  36244  cbvixpdavw2  36260  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  dibfnN  41113  dihintcl  41301  frlmvscadiccat  42461  selvvvval  42540  ofoafg  43316  uzmptshftfval  44315  srhmsubcALTV  48048