Theorem fneq2d 6663

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566

This theorem is referenced by:  fneq12d  6664  fncofn  6686  fnco  6687  fnprb  7228  fntpb  7229  fnpr2g  7230  undifixp  8973  brwdom2  9611  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  dfac3  10159  ac7g  10512  ccatlid  14621  ccatrid  14622  ccatass  14623  ccatswrd  14703  swrdccat2  14704  ccatpfx  14736  swrdswrd  14740  swrdccatin2  14764  pfxccatin12  14768  revccat  14801  revrev  14802  repsdf2  14813  0csh0  14828  cshco  14872  wrd2pr2op  14979  wrd3tpop  14984  ofccat  15005  seqshft  15121  invf  17816  sscfn1  17865  sscfn2  17866  isssc  17868  fuchom  18017  fuchomOLD  18018  estrchomfeqhom  18191  mulgfval  19100  mulgfvalALT  19101  srhmsubc  20697  frlmsslss2  21813  subrgascl  22108  m1detdiag  22619  ptval  23594  xpsdsfn2  24404  fresf1o  32648  psgndmfi  33101  cycpmconjslem1  33157  cycpmconjslem2  33158  ply1annidllem  33709  pl1cn  33916  signsvtn0  34564  signstres  34569  bnj927  34762  fineqvac  35090  revpfxsfxrev  35100  ixpeq12dv  36199  cbvixpdavw  36261  cbvixpdavw2  36277  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem11  37618  poimirlem12  37619  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  dibfnN  41139  dihintcl  41327  frlmvscadiccat  42493  selvvvval  42572  ofoafg  43344  uzmptshftfval  44342  srhmsubcALTV  48169