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  14614  ccatrid  14615  ccatass  14616  ccatswrd  14696  swrdccat2  14697  ccatpfx  14728  swrdswrd  14732  swrdccatin2  14756  pfxccatin12  14760  revccat  14793  revrev  14794  repsdf2  14805  0csh0  14820  cshco  14863  wrd2pr2op  14970  wrd3tpop  14975  ofccat  14996  seqshft  15112  invf  17815  sscfn1  17864  sscfn2  17865  isssc  17867  fuchom  18011  estrchomfeqhom  18182  mulgfval  19126  mulgfvalALT  19127  srhmsubc  20756  frlmsslss2  21885  subrgascl  22177  selvvvval  22253  m1detdiag  22715  ptval  23688  xpsdsfn2  24496  fresf1o  32888  psgndmfi  33331  cycpmconjslem1  33387  cycpmconjslem2  33388  ply1annidllem  34008  pl1cn  34262  signsvtn0  34874  signstres  34879  bnj927  35075  fineqvac  35424  revpfxsfxrev  35478  ixpeq12dv  36589  cbvixpdavw  36651  cbvixpdavw2  36667  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem6  38137  poimirlem7  38138  poimirlem11  38142  poimirlem12  38143  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  dibfnN  41792  dihintcl  41980  frlmvscadiccat  43140  ofoafg  43943  uzmptshftfval  44920  srhmsubcALTV  48945  tposideq  49517  nelsubc3lem  49699  0funcg2  49713  fucofulem2  49940  termcfuncval  50161  termcnatval  50164  0fucterm  50172  cnelsubclem  50232