Theorem fneq2d 6643

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   Fn wfn 6538

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6546

This theorem is referenced by:  fneq12d  6644  fncofn  6666  fnco  6667  fnprb  7212  fntpb  7213  fnpr2g  7214  undifixp  8930  brwdom2  9570  brttrcl2  9711  ssttrcl  9712  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  dfac3  10118  ac7g  10471  ccatlid  14540  ccatrid  14541  ccatass  14542  ccatswrd  14622  swrdccat2  14623  ccatpfx  14655  swrdswrd  14659  swrdccatin2  14683  pfxccatin12  14687  revccat  14720  revrev  14721  repsdf2  14732  0csh0  14747  cshco  14791  wrd2pr2op  14898  wrd3tpop  14903  ofccat  14920  seqshft  15036  invf  17719  sscfn1  17768  sscfn2  17769  isssc  17771  fuchom  17917  fuchomOLD  17918  estrchomfeqhom  18091  mulgfval  18988  mulgfvalALT  18989  frlmsslss2  21549  subrgascl  21846  m1detdiag  22319  ptval  23294  xpsdsfn2  24104  fresf1o  32110  psgndmfi  32515  cycpmconjslem1  32571  cycpmconjslem2  32572  ply1annidllem  33039  pl1cn  33221  signsvtn0  33867  signstres  33872  bnj927  34066  fineqvac  34383  revpfxsfxrev  34392  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem11  36802  poimirlem12  36803  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  dibfnN  40330  dihintcl  40518  frlmvscadiccat  41386  selvvvval  41459  ofoafg  42406  uzmptshftfval  43407  srhmsubc  47063  srhmsubcALTV  47081