Theorem fneq2d 6631

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541

This theorem is referenced by:  fneq12d  6632  fncofn  6654  fnco  6655  fnprb  7208  fntpb  7209  fnpr2g  7210  undifixp  8933  brwdom2  9536  brttrcl2  9684  ssttrcl  9685  ttrcltr  9686  ttrclss  9690  ttrclselem2  9696  dfac3  10106  ac7g  10459  ccatlid  14626  ccatrid  14627  ccatass  14628  ccatswrd  14708  swrdccat2  14709  ccatpfx  14740  swrdswrd  14744  swrdccatin2  14768  pfxccatin12  14772  revccat  14805  revrev  14806  repsdf2  14817  0csh0  14832  cshco  14875  wrd2pr2op  14982  wrd3tpop  14987  ofccat  15008  seqshft  15124  invf  17826  sscfn1  17875  sscfn2  17876  isssc  17878  fuchom  18022  estrchomfeqhom  18193  mulgfval  19136  mulgfvalALT  19137  srhmsubc  20766  frlmsslss2  21906  subrgascl  22198  selvvvval  22274  m1detdiag  22735  ptval  23708  xpsdsfn2  24516  fresf1o  32957  psgndmfi  33399  cycpmconjslem1  33455  cycpmconjslem2  33456  ply1annidllem  34072  pl1cn  34326  signsvtn0  34938  signstres  34943  bnj927  35139  fineqvac  35510  revpfxsfxrev  35588  ixpeq12dv  36709  cbvixpdavw  36771  cbvixpdavw2  36787  poimirlem1  38253  poimirlem2  38254  poimirlem3  38255  poimirlem4  38256  poimirlem6  38258  poimirlem7  38259  poimirlem11  38263  poimirlem12  38264  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  dibfnN  41911  dihintcl  42099  frlmvscadiccat  43261  ofoafg  44064  uzmptshftfval  45039  srhmsubcALTV  49073  tposideq  49649  nelsubc3lem  49831  0funcg2  49845  fucofulem2  50072  termcfuncval  50293  termcnatval  50296  0fucterm  50304  cnelsubclem  50364