Theorem fneq2d 6662

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564

This theorem is referenced by:  fneq12d  6663  fncofn  6685  fnco  6686  fnprb  7228  fntpb  7229  fnpr2g  7230  undifixp  8974  brwdom2  9613  brttrcl2  9754  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  dfac3  10161  ac7g  10514  ccatlid  14624  ccatrid  14625  ccatass  14626  ccatswrd  14706  swrdccat2  14707  ccatpfx  14739  swrdswrd  14743  swrdccatin2  14767  pfxccatin12  14771  revccat  14804  revrev  14805  repsdf2  14816  0csh0  14831  cshco  14875  wrd2pr2op  14982  wrd3tpop  14987  ofccat  15008  seqshft  15124  invf  17812  sscfn1  17861  sscfn2  17862  isssc  17864  fuchom  18009  estrchomfeqhom  18180  mulgfval  19087  mulgfvalALT  19088  srhmsubc  20680  frlmsslss2  21795  subrgascl  22090  m1detdiag  22603  ptval  23578  xpsdsfn2  24388  fresf1o  32641  psgndmfi  33118  cycpmconjslem1  33174  cycpmconjslem2  33175  ply1annidllem  33744  pl1cn  33954  signsvtn0  34585  signstres  34590  bnj927  34783  fineqvac  35111  revpfxsfxrev  35121  ixpeq12dv  36217  cbvixpdavw  36279  cbvixpdavw2  36295  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  dibfnN  41158  dihintcl  41346  frlmvscadiccat  42516  selvvvval  42595  ofoafg  43367  uzmptshftfval  44365  srhmsubcALTV  48241  tposideq  48788  0funcg2  48917  fucofulem2  49006