Theorem fneq2d 6434

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539   Fn wfn 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1783  df-cleq 2751  df-fn 6344

This theorem is referenced by:  fneq12d  6435  fnprb  6969  fntpb  6970  fnpr2g  6971  undifixp  8530  brwdom2  9084  dfac3  9595  ac7g  9948  ccatlid  14001  ccatrid  14002  ccatass  14003  ccatswrd  14091  swrdccat2  14092  ccatpfx  14124  swrdswrd  14128  swrdccatin2  14152  pfxccatin12  14156  revccat  14189  revrev  14190  repsdf2  14201  0csh0  14216  cshco  14259  wrd2pr2op  14366  wrd3tpop  14371  ofccat  14390  seqshft  14506  invf  17112  sscfn1  17161  sscfn2  17162  isssc  17164  fuchom  17305  estrchomfeqhom  17467  mulgfval  18308  mulgfvalALT  18309  frlmsslss2  20555  subrgascl  20842  m1detdiag  21312  ptval  22285  xpsdsfn2  23095  fresf1o  30503  psgndmfi  30905  cycpmconjslem1  30961  cycpmconjslem2  30962  pl1cn  31440  signsvtn0  32082  signstres  32087  bnj927  32282  revpfxsfxrev  32607  poimirlem1  35374  poimirlem2  35375  poimirlem3  35376  poimirlem4  35377  poimirlem6  35379  poimirlem7  35380  poimirlem11  35384  poimirlem12  35385  poimirlem16  35389  poimirlem17  35390  poimirlem19  35392  poimirlem20  35393  dibfnN  38768  dihintcl  38956  frlmvscadiccat  39784  uzmptshftfval  41469  srhmsubc  45127  srhmsubcALTV  45145