Theorem fneq2d 6580

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

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

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 2705

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

This theorem is referenced by:  fneq12d  6581  fncofn  6603  fnco  6604  fnprb  7148  fntpb  7149  fnpr2g  7150  undifixp  8864  brwdom2  9466  brttrcl2  9611  ssttrcl  9612  ttrcltr  9613  ttrclss  9617  ttrclselem2  9623  dfac3  10019  ac7g  10372  ccatlid  14496  ccatrid  14497  ccatass  14498  ccatswrd  14578  swrdccat2  14579  ccatpfx  14610  swrdswrd  14614  swrdccatin2  14638  pfxccatin12  14642  revccat  14675  revrev  14676  repsdf2  14687  0csh0  14702  cshco  14745  wrd2pr2op  14852  wrd3tpop  14857  ofccat  14878  seqshft  14994  invf  17677  sscfn1  17726  sscfn2  17727  isssc  17729  fuchom  17873  estrchomfeqhom  18044  mulgfval  18984  mulgfvalALT  18985  srhmsubc  20597  frlmsslss2  21714  subrgascl  22002  m1detdiag  22513  ptval  23486  xpsdsfn2  24294  fresf1o  32615  psgndmfi  33074  cycpmconjslem1  33130  cycpmconjslem2  33131  ply1annidllem  33735  pl1cn  33989  signsvtn0  34604  signstres  34609  bnj927  34802  fineqvac  35160  revpfxsfxrev  35181  ixpeq12dv  36281  cbvixpdavw  36343  cbvixpdavw2  36359  poimirlem1  37682  poimirlem2  37683  poimirlem3  37684  poimirlem4  37685  poimirlem6  37687  poimirlem7  37688  poimirlem11  37692  poimirlem12  37693  poimirlem16  37697  poimirlem17  37698  poimirlem19  37700  poimirlem20  37701  dibfnN  41276  dihintcl  41464  frlmvscadiccat  42625  selvvvval  42704  ofoafg  43472  uzmptshftfval  44464  srhmsubcALTV  48450  tposideq  49013  nelsubc3lem  49196  0funcg2  49210  fucofulem2  49437  termcfuncval  49658  termcnatval  49661  0fucterm  49669  cnelsubclem  49729