Theorem fneq2d 6580

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6489

This theorem is referenced by:  fneq12d  6581  fncofn  6603  fnco  6604  fnprb  7148  fntpb  7149  fnpr2g  7150  undifixp  8868  brwdom2  9484  brttrcl2  9629  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  dfac3  10034  ac7g  10387  ccatlid  14511  ccatrid  14512  ccatass  14513  ccatswrd  14593  swrdccat2  14594  ccatpfx  14625  swrdswrd  14629  swrdccatin2  14653  pfxccatin12  14657  revccat  14690  revrev  14691  repsdf2  14702  0csh0  14717  cshco  14761  wrd2pr2op  14868  wrd3tpop  14873  ofccat  14894  seqshft  15010  invf  17693  sscfn1  17742  sscfn2  17743  isssc  17745  fuchom  17889  estrchomfeqhom  18060  mulgfval  18966  mulgfvalALT  18967  srhmsubc  20583  frlmsslss2  21700  subrgascl  21989  m1detdiag  22500  ptval  23473  xpsdsfn2  24282  fresf1o  32588  psgndmfi  33053  cycpmconjslem1  33109  cycpmconjslem2  33110  ply1annidllem  33670  pl1cn  33924  signsvtn0  34540  signstres  34545  bnj927  34738  fineqvac  35074  revpfxsfxrev  35091  ixpeq12dv  36192  cbvixpdavw  36254  cbvixpdavw2  36270  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem11  37613  poimirlem12  37614  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  dibfnN  41138  dihintcl  41326  frlmvscadiccat  42482  selvvvval  42561  ofoafg  43330  uzmptshftfval  44322  srhmsubcALTV  48313  tposideq  48876  nelsubc3lem  49059  0funcg2  49073  fucofulem2  49300  termcfuncval  49521  termcnatval  49524  0fucterm  49532  cnelsubclem  49592