Theorem fneq2d 6633

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6541

This theorem is used by:  fneq12d  6634  fncofn  6656  fnco  6657  fnprb  7214  fntpb  7215  fnpr2g  7216  undifixp  8965  brwdom2  9570  brttrcl2  9718  ssttrcl  9719  ttrcltr  9720  ttrclss  9724  ttrclselem2  9730  dfac3  10203  ac7g  10555  ccatlid  14735  ccatrid  14736  ccatass  14737  ccatswrd  14822  swrdccat2  14823  ccatpfx  14854  swrdswrd  14858  swrdccatin2  14882  pfxccatin12  14886  revccat  14919  revrev  14920  revpfxsfxrev  14921  repsdf2  14933  0csh0  14948  cshco  14991  wrd2pr2op  15099  wrd3tpop  15104  ofccat  15127  seqshft  15243  invf  17948  sscfn1  17997  sscfn2  17998  isssc  18000  fuchom  18144  estrchomfeqhom  18315  mulgfval  19284  mulgfvalALT  19285  srhmsubc  20937  frlmsslss2  22086  subrgascl  22380  selvvvval  22456  m1detdiag  22917  ptval  23894  xpsdsfn2  24702  fresf1o  33272  psgndmfi  33705  cycpmconjslem1  33761  cycpmconjslem2  33762  ply1annidllem  34379  pl1cn  34633  signsvtn0  35245  signstres  35250  bnj927  35446  fineqvac  35840  ixpeq12dv  37097  cbvixpdavw  37159  cbvixpdavw2  37175  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem6  38637  poimirlem7  38638  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  dibfnN  42306  dihintcl  42494  frlmvscadiccat  43666  ofoafg  44449  uzmptshftfval  45423  srhmsubcALTV  49515  tposideq  50094  nelsubc3lem  50277  0funcg2  50292  fucofulem2  50526  termcfuncval  50760  termcnatval  50766  0fucterm  50774  cnelsubcw  50834