Theorem fneq2d 6449

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   Fn wfn 6352

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 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-fn 6360

This theorem is referenced by:  fneq12d  6450  fnprb  6973  fntpb  6974  fnpr2g  6975  undifixp  8500  brwdom2  9039  dfac3  9549  ac7g  9898  ccatlid  13942  ccatrid  13943  ccatass  13944  ccatswrd  14032  swrdccat2  14033  ccatpfx  14065  swrdswrd  14069  swrdccatin2  14093  pfxccatin12  14097  revccat  14130  revrev  14131  repsdf2  14142  0csh0  14157  cshco  14200  wrd2pr2op  14307  wrd3tpop  14312  ofccat  14331  seqshft  14446  invf  17040  sscfn1  17089  sscfn2  17090  isssc  17092  fuchom  17233  estrchomfeqhom  17388  mulgfval  18228  mulgfvalALT  18229  subrgascl  20280  frlmsslss2  20921  m1detdiag  21208  ptval  22180  xpsdsfn2  22990  fresf1o  30378  psgndmfi  30742  cycpmconjslem1  30798  cycpmconjslem2  30799  pl1cn  31200  signsvtn0  31842  signstres  31847  bnj927  32042  revpfxsfxrev  32364  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem11  34905  poimirlem12  34906  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  dibfnN  38294  dihintcl  38482  frlmvscadiccat  39152  uzmptshftfval  40685  srhmsubc  44354  srhmsubcALTV  44372