Theorem fneq2d 6536

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

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

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-fn 6440

This theorem is referenced by:  fneq12d  6537  fncofn  6557  fnco  6558  fnprb  7093  fntpb  7094  fnpr2g  7095  undifixp  8731  brwdom2  9341  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  dfac3  9886  ac7g  10239  ccatlid  14300  ccatrid  14301  ccatass  14302  ccatswrd  14390  swrdccat2  14391  ccatpfx  14423  swrdswrd  14427  swrdccatin2  14451  pfxccatin12  14455  revccat  14488  revrev  14489  repsdf2  14500  0csh0  14515  cshco  14558  wrd2pr2op  14665  wrd3tpop  14670  ofccat  14689  seqshft  14805  invf  17489  sscfn1  17538  sscfn2  17539  isssc  17541  fuchom  17687  fuchomOLD  17688  estrchomfeqhom  17861  mulgfval  18711  mulgfvalALT  18712  frlmsslss2  20991  subrgascl  21283  m1detdiag  21755  ptval  22730  xpsdsfn2  23540  fresf1o  30975  psgndmfi  31374  cycpmconjslem1  31430  cycpmconjslem2  31431  pl1cn  31914  signsvtn0  32558  signstres  32563  bnj927  32758  fineqvac  33075  revpfxsfxrev  33086  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  dibfnN  39177  dihintcl  39365  frlmvscadiccat  40244  uzmptshftfval  41971  srhmsubc  45645  srhmsubcALTV  45663