Theorem fneq2d 6611

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   Fn wfn 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6520

This theorem is referenced by:  fneq12d  6612  fncofn  6634  fnco  6635  fnprb  7188  fntpb  7189  fnpr2g  7190  undifixp  8912  brwdom2  9518  brttrcl2  9666  ssttrcl  9667  ttrcltr  9668  ttrclss  9672  ttrclselem2  9678  dfac3  10074  ac7g  10428  ccatlid  14597  ccatrid  14598  ccatass  14599  ccatswrd  14679  swrdccat2  14680  ccatpfx  14711  swrdswrd  14715  swrdccatin2  14739  pfxccatin12  14743  revccat  14776  revrev  14777  repsdf2  14788  0csh0  14803  cshco  14846  wrd2pr2op  14953  wrd3tpop  14958  ofccat  14979  seqshft  15095  invf  17784  sscfn1  17833  sscfn2  17834  isssc  17836  fuchom  17980  estrchomfeqhom  18151  mulgfval  19094  mulgfvalALT  19095  srhmsubc  20709  frlmsslss2  21807  subrgascl  22099  selvvvval  22175  m1detdiag  22637  ptval  23610  xpsdsfn2  24418  fresf1o  32783  psgndmfi  33239  cycpmconjslem1  33295  cycpmconjslem2  33296  ply1annidllem  33959  pl1cn  34213  signsvtn0  34828  signstres  34833  bnj927  35029  fineqvac  35376  revpfxsfxrev  35430  ixpeq12dv  36540  cbvixpdavw  36602  cbvixpdavw2  36618  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem6  38089  poimirlem7  38090  poimirlem11  38094  poimirlem12  38095  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  dibfnN  41744  dihintcl  41932  frlmvscadiccat  43092  ofoafg  43895  uzmptshftfval  44886  srhmsubcALTV  48911  tposideq  49473  nelsubc3lem  49655  0funcg2  49669  fucofulem2  49896  termcfuncval  50117  termcnatval  50120  0fucterm  50128  cnelsubclem  50188