Theorem fneq2d 6644

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   Fn wfn 6539

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6547

This theorem is referenced by:  fneq12d  6645  fncofn  6667  fnco  6668  fnprb  7210  fntpb  7211  fnpr2g  7212  undifixp  8928  brwdom2  9568  brttrcl2  9709  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  dfac3  10116  ac7g  10469  ccatlid  14536  ccatrid  14537  ccatass  14538  ccatswrd  14618  swrdccat2  14619  ccatpfx  14651  swrdswrd  14655  swrdccatin2  14679  pfxccatin12  14683  revccat  14716  revrev  14717  repsdf2  14728  0csh0  14743  cshco  14787  wrd2pr2op  14894  wrd3tpop  14899  ofccat  14916  seqshft  15032  invf  17715  sscfn1  17764  sscfn2  17765  isssc  17767  fuchom  17913  fuchomOLD  17914  estrchomfeqhom  18087  mulgfval  18952  mulgfvalALT  18953  frlmsslss2  21330  subrgascl  21627  m1detdiag  22099  ptval  23074  xpsdsfn2  23884  fresf1o  31855  psgndmfi  32257  cycpmconjslem1  32313  cycpmconjslem2  32314  ply1annidllem  32762  pl1cn  32935  signsvtn0  33581  signstres  33586  bnj927  33780  fineqvac  34097  revpfxsfxrev  34106  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  dibfnN  40027  dihintcl  40215  frlmvscadiccat  41080  selvvvval  41157  ofoafg  42104  uzmptshftfval  43105  srhmsubc  46974  srhmsubcALTV  46992