Theorem fneq2d 6615

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

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

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 2702

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

This theorem is referenced by:  fneq12d  6616  fncofn  6638  fnco  6639  fnprb  7185  fntpb  7186  fnpr2g  7187  undifixp  8910  brwdom2  9533  brttrcl2  9674  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  dfac3  10081  ac7g  10434  ccatlid  14558  ccatrid  14559  ccatass  14560  ccatswrd  14640  swrdccat2  14641  ccatpfx  14673  swrdswrd  14677  swrdccatin2  14701  pfxccatin12  14705  revccat  14738  revrev  14739  repsdf2  14750  0csh0  14765  cshco  14809  wrd2pr2op  14916  wrd3tpop  14921  ofccat  14942  seqshft  15058  invf  17737  sscfn1  17786  sscfn2  17787  isssc  17789  fuchom  17933  estrchomfeqhom  18104  mulgfval  19008  mulgfvalALT  19009  srhmsubc  20596  frlmsslss2  21691  subrgascl  21980  m1detdiag  22491  ptval  23464  xpsdsfn2  24273  fresf1o  32562  psgndmfi  33062  cycpmconjslem1  33118  cycpmconjslem2  33119  ply1annidllem  33698  pl1cn  33952  signsvtn0  34568  signstres  34573  bnj927  34766  fineqvac  35094  revpfxsfxrev  35110  ixpeq12dv  36211  cbvixpdavw  36273  cbvixpdavw2  36289  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  dibfnN  41157  dihintcl  41345  frlmvscadiccat  42501  selvvvval  42580  ofoafg  43350  uzmptshftfval  44342  srhmsubcALTV  48317  tposideq  48880  nelsubc3lem  49063  0funcg2  49077  fucofulem2  49304  termcfuncval  49525  termcnatval  49528  0fucterm  49536  cnelsubclem  49596