Theorem fneq2d 6658

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   Fn wfn 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6564

This theorem is used by:  fneq12d  6659  fncofn  6681  fnco  6682  fnprb  7240  fntpb  7241  fnpr2g  7242  undifixp  8993  brwdom2  9597  brttrcl2  9745  ssttrcl  9746  ttrcltr  9747  ttrclss  9751  ttrclselem2  9757  dfac3  10230  ac7g  10582  ccatlid  14762  ccatrid  14763  ccatass  14764  ccatswrd  14849  swrdccat2  14850  ccatpfx  14881  swrdswrd  14885  swrdccatin2  14909  pfxccatin12  14913  revccat  14946  revrev  14947  revpfxsfxrev  14948  repsdf2  14960  0csh0  14975  cshco  15018  wrd2pr2op  15126  wrd3tpop  15131  ofccat  15154  seqshft  15270  invf  17975  sscfn1  18024  sscfn2  18025  isssc  18027  fuchom  18171  estrchomfeqhom  18342  mulgfval  19311  mulgfvalALT  19312  srhmsubc  20965  frlmsslss2  22114  subrgascl  22408  selvvvval  22484  m1detdiag  22945  ptval  23922  xpsdsfn2  24730  fresf1o  33300  psgndmfi  33735  cycpmconjslem1  33791  cycpmconjslem2  33792  ply1annidllem  34416  pl1cn  34670  signsvtn0  35282  signstres  35287  bnj927  35483  fineqvac  35897  ixpeq12dv  37196  cbvixpdavw  37258  cbvixpdavw2  37274  poimirlem1  38744  poimirlem2  38745  poimirlem3  38746  poimirlem4  38747  poimirlem6  38749  poimirlem7  38750  poimirlem11  38754  poimirlem12  38755  poimirlem16  38759  poimirlem17  38760  poimirlem19  38762  poimirlem20  38763  dibfnN  42416  dihintcl  42604  frlmvscadiccat  43777  ofoafg  44559  uzmptshftfval  45533  srhmsubcALTV  49637  tposideq  50216  nelsubc3lem  50399  0funcg2  50414  fucofulem2  50648  termcfuncval  50882  termcnatval  50888  0fucterm  50896  cnelsubcw  50956