Theorem fneq2d 6619

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-fn 6528

This theorem is referenced by:  fneq12d  6620  fncofn  6642  fnco  6643  fnprb  7196  fntpb  7197  fnpr2g  7198  undifixp  8920  brwdom2  9523  brttrcl2  9671  ssttrcl  9672  ttrcltr  9673  ttrclss  9677  ttrclselem2  9683  dfac3  10093  ac7g  10446  ccatlid  14612  ccatrid  14613  ccatass  14614  ccatswrd  14694  swrdccat2  14695  ccatpfx  14726  swrdswrd  14730  swrdccatin2  14754  pfxccatin12  14758  revccat  14791  revrev  14792  repsdf2  14803  0csh0  14818  cshco  14861  wrd2pr2op  14968  wrd3tpop  14973  ofccat  14994  seqshft  15110  invf  17813  sscfn1  17862  sscfn2  17863  isssc  17865  fuchom  18009  estrchomfeqhom  18180  mulgfval  19123  mulgfvalALT  19124  srhmsubc  20753  frlmsslss2  21882  subrgascl  22174  selvvvval  22250  m1detdiag  22711  ptval  23684  xpsdsfn2  24492  fresf1o  32884  psgndmfi  33326  cycpmconjslem1  33382  cycpmconjslem2  33383  ply1annidllem  34003  pl1cn  34257  signsvtn0  34869  signstres  34874  bnj927  35070  fineqvac  35419  revpfxsfxrev  35473  ixpeq12dv  36584  cbvixpdavw  36646  cbvixpdavw2  36662  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem4  38130  poimirlem6  38132  poimirlem7  38133  poimirlem11  38137  poimirlem12  38138  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  dibfnN  41787  dihintcl  41975  frlmvscadiccat  43135  ofoafg  43938  uzmptshftfval  44915  srhmsubcALTV  48946  tposideq  49518  nelsubc3lem  49700  0funcg2  49714  fucofulem2  49941  termcfuncval  50162  termcnatval  50165  0fucterm  50173  cnelsubclem  50233