Theorem fneq2d 6511

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421

This theorem is referenced by:  fneq12d  6512  fncofn  6532  fnco  6533  fnprb  7066  fntpb  7067  fnpr2g  7068  undifixp  8680  brwdom2  9262  dfac3  9808  ac7g  10161  ccatlid  14219  ccatrid  14220  ccatass  14221  ccatswrd  14309  swrdccat2  14310  ccatpfx  14342  swrdswrd  14346  swrdccatin2  14370  pfxccatin12  14374  revccat  14407  revrev  14408  repsdf2  14419  0csh0  14434  cshco  14477  wrd2pr2op  14584  wrd3tpop  14589  ofccat  14608  seqshft  14724  invf  17397  sscfn1  17446  sscfn2  17447  isssc  17449  fuchom  17594  fuchomOLD  17595  estrchomfeqhom  17768  mulgfval  18617  mulgfvalALT  18618  frlmsslss2  20892  subrgascl  21184  m1detdiag  21654  ptval  22629  xpsdsfn2  23439  fresf1o  30867  psgndmfi  31267  cycpmconjslem1  31323  cycpmconjslem2  31324  pl1cn  31807  signsvtn0  32449  signstres  32454  bnj927  32649  fineqvac  32966  revpfxsfxrev  32977  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  dibfnN  39097  dihintcl  39285  frlmvscadiccat  40163  uzmptshftfval  41853  srhmsubc  45522  srhmsubcALTV  45540