Theorem fneq2d 6612

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

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

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 6514

This theorem is referenced by:  fneq12d  6613  fncofn  6635  fnco  6636  fnprb  7182  fntpb  7183  fnpr2g  7184  undifixp  8907  brwdom2  9526  brttrcl2  9667  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  dfac3  10074  ac7g  10427  ccatlid  14551  ccatrid  14552  ccatass  14553  ccatswrd  14633  swrdccat2  14634  ccatpfx  14666  swrdswrd  14670  swrdccatin2  14694  pfxccatin12  14698  revccat  14731  revrev  14732  repsdf2  14743  0csh0  14758  cshco  14802  wrd2pr2op  14909  wrd3tpop  14914  ofccat  14935  seqshft  15051  invf  17730  sscfn1  17779  sscfn2  17780  isssc  17782  fuchom  17926  estrchomfeqhom  18097  mulgfval  19001  mulgfvalALT  19002  srhmsubc  20589  frlmsslss2  21684  subrgascl  21973  m1detdiag  22484  ptval  23457  xpsdsfn2  24266  fresf1o  32555  psgndmfi  33055  cycpmconjslem1  33111  cycpmconjslem2  33112  ply1annidllem  33691  pl1cn  33945  signsvtn0  34561  signstres  34566  bnj927  34759  fineqvac  35087  revpfxsfxrev  35103  ixpeq12dv  36204  cbvixpdavw  36266  cbvixpdavw2  36282  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  dibfnN  41150  dihintcl  41338  frlmvscadiccat  42494  selvvvval  42573  ofoafg  43343  uzmptshftfval  44335  srhmsubcALTV  48313  tposideq  48876  nelsubc3lem  49059  0funcg2  49073  fucofulem2  49300  termcfuncval  49521  termcnatval  49524  0fucterm  49532  cnelsubclem  49592