Theorem fneq2d 6575

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484

This theorem is referenced by:  fneq12d  6576  fncofn  6598  fnco  6599  fnprb  7142  fntpb  7143  fnpr2g  7144  undifixp  8858  brwdom2  9459  brttrcl2  9604  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  ttrclselem2  9616  dfac3  10012  ac7g  10365  ccatlid  14494  ccatrid  14495  ccatass  14496  ccatswrd  14576  swrdccat2  14577  ccatpfx  14608  swrdswrd  14612  swrdccatin2  14636  pfxccatin12  14640  revccat  14673  revrev  14674  repsdf2  14685  0csh0  14700  cshco  14743  wrd2pr2op  14850  wrd3tpop  14855  ofccat  14876  seqshft  14992  invf  17675  sscfn1  17724  sscfn2  17725  isssc  17727  fuchom  17871  estrchomfeqhom  18042  mulgfval  18982  mulgfvalALT  18983  srhmsubc  20596  frlmsslss2  21713  subrgascl  22002  m1detdiag  22513  ptval  23486  xpsdsfn2  24294  fresf1o  32611  psgndmfi  33065  cycpmconjslem1  33121  cycpmconjslem2  33122  ply1annidllem  33712  pl1cn  33966  signsvtn0  34581  signstres  34586  bnj927  34779  fineqvac  35137  revpfxsfxrev  35158  ixpeq12dv  36256  cbvixpdavw  36318  cbvixpdavw2  36334  poimirlem1  37667  poimirlem2  37668  poimirlem3  37669  poimirlem4  37670  poimirlem6  37672  poimirlem7  37673  poimirlem11  37677  poimirlem12  37678  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  dibfnN  41201  dihintcl  41389  frlmvscadiccat  42545  selvvvval  42624  ofoafg  43393  uzmptshftfval  44385  srhmsubcALTV  48362  tposideq  48925  nelsubc3lem  49108  0funcg2  49122  fucofulem2  49349  termcfuncval  49570  termcnatval  49573  0fucterm  49581  cnelsubclem  49641