Theorem fneq2d 6625

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6534

This theorem is used by:  fneq12d  6626  fncofn  6648  fnco  6649  fnprb  7206  fntpb  7207  fnpr2g  7208  undifixp  8946  brwdom2  9551  brttrcl2  9699  ssttrcl  9700  ttrcltr  9701  ttrclss  9705  ttrclselem2  9711  dfac3  10181  ac7g  10533  ccatlid  14712  ccatrid  14713  ccatass  14714  ccatswrd  14798  swrdccat2  14799  ccatpfx  14830  swrdswrd  14834  swrdccatin2  14858  pfxccatin12  14862  revccat  14895  revrev  14896  revpfxsfxrev  14897  repsdf2  14909  0csh0  14924  cshco  14967  wrd2pr2op  15074  wrd3tpop  15079  ofccat  15102  seqshft  15218  invf  17923  sscfn1  17972  sscfn2  17973  isssc  17975  fuchom  18119  estrchomfeqhom  18290  mulgfval  19259  mulgfvalALT  19260  srhmsubc  20912  frlmsslss2  22061  subrgascl  22355  selvvvval  22431  m1detdiag  22892  ptval  23869  xpsdsfn2  24677  fresf1o  33207  psgndmfi  33641  cycpmconjslem1  33697  cycpmconjslem2  33698  ply1annidllem  34315  pl1cn  34569  signsvtn0  35182  signstres  35187  bnj927  35383  fineqvac  35757  ixpeq12dv  36975  cbvixpdavw  37037  cbvixpdavw2  37053  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem6  38512  poimirlem7  38513  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  dibfnN  42181  dihintcl  42369  frlmvscadiccat  43538  ofoafg  44314  uzmptshftfval  45289  srhmsubcALTV  49366  tposideq  49940  nelsubc3lem  50122  0funcg2  50136  fucofulem2  50363  termcfuncval  50584  termcnatval  50587  0fucterm  50595  cnelsubclem  50655