Theorem fneq2d 6594

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503

This theorem is referenced by:  fneq12d  6595  fncofn  6617  fnco  6618  fnprb  7164  fntpb  7165  fnpr2g  7166  undifixp  8884  brwdom2  9490  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  dfac3  10043  ac7g  10396  ccatlid  14522  ccatrid  14523  ccatass  14524  ccatswrd  14604  swrdccat2  14605  ccatpfx  14636  swrdswrd  14640  swrdccatin2  14664  pfxccatin12  14668  revccat  14701  revrev  14702  repsdf2  14713  0csh0  14728  cshco  14771  wrd2pr2op  14878  wrd3tpop  14883  ofccat  14904  seqshft  15020  invf  17704  sscfn1  17753  sscfn2  17754  isssc  17756  fuchom  17900  estrchomfeqhom  18071  mulgfval  19011  mulgfvalALT  19012  srhmsubc  20625  frlmsslss2  21742  subrgascl  22033  m1detdiag  22553  ptval  23526  xpsdsfn2  24334  fresf1o  32720  psgndmfi  33191  cycpmconjslem1  33247  cycpmconjslem2  33248  ply1annidllem  33878  pl1cn  34132  signsvtn0  34747  signstres  34752  bnj927  34945  fineqvac  35291  revpfxsfxrev  35329  ixpeq12dv  36429  cbvixpdavw  36491  cbvixpdavw2  36507  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem6  37874  poimirlem7  37875  poimirlem11  37879  poimirlem12  37880  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  dibfnN  41529  dihintcl  41717  frlmvscadiccat  42873  selvvvval  42940  ofoafg  43708  uzmptshftfval  44699  srhmsubcALTV  48682  tposideq  49244  nelsubc3lem  49426  0funcg2  49440  fucofulem2  49667  termcfuncval  49888  termcnatval  49891  0fucterm  49899  cnelsubclem  49959