Theorem ineq2d 4139

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ineq2d	⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Proof of Theorem ineq2d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq2 4133	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1538   ∩ cin 3880

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-in 3888

This theorem is referenced by:  rint0  4878  riin0  4967  disji2  5012  disjprgw  5025  disjprg  5026  disjxun  5028  xpriindi  5671  riinint  5804  reseq2  5813  resindm  5867  predep  6142  onfr  6198  fimacnvinrn  6817  fimacnvinrn2  6818  isofrlem  7072  isoselem  7073  oev2  8131  domss2  8660  funsnfsupp  8841  kmlem11  9571  fpwwe2cbv  10041  fpwwe2lem3  10044  fpwwe2lem8  10048  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  fz1isolem  13815  limsupgle  14826  fsumm1  15098  incexclem  15183  bitsinv1  15781  bitsinvp1  15788  sadcadd  15797  sadadd2  15799  smumullem  15831  ressbas  16546  ressress  16554  restval  16692  ismred2  16866  resscatc  17357  cnvps  17814  cntziinsn  18457  lsmdisj3r  18804  lsmdisj3b  18808  gsummptfzsplitl  19046  dmdprd  19113  subgdmdprd  19149  pgpfaclem1  19196  subrgpropd  19563  crng2idl  20005  obselocv  20417  basis1  21555  baspartn  21559  eltg  21562  tgdom  21583  indistopon  21606  ntrval  21641  clslp  21753  resttopon2  21773  restopnb  21780  paste  21899  nrmsep3  21960  imacmp  22002  cmpsub  22005  bwth  22015  llyi  22079  nllyi  22080  cldllycmp  22100  kgencmp2  22151  ptbasfi  22186  kqdisj  22337  kqcldsat  22338  trfbas2  22448  filss  22458  elfg  22476  flimclslem  22589  fcfneii  22642  tsmsfbas  22733  restutopopn  22844  ressxms  23132  restmetu  23177  qtopbaslem  23364  pi1addf  23652  pi1addval  23653  shftmbl  24142  voliunlem1  24154  voliunlem2  24155  uniioombllem2  24187  uniioombllem4  24190  uniioombllem6  24192  volsup2  24209  volcn  24210  volivth  24211  itg1climres  24318  limciun  24497  dvres3a  24517  ig1pval  24773  p1evtxdeqlem  27302  pthdlem2  27557  eupthp1  28001  omlsi  29187  pjoml  29219  chdmj3  29314  chdmj4  29315  ledi  29323  cmbr  29367  cmbr3  29391  pjoml3  29395  fh1  29401  fh2  29402  dmdbr  30082  dmdmd  30083  dmdbr5  30091  dmdsl3  30098  chirredlem2  30174  chirredlem3  30175  dmdbr6ati  30206  unidifsnne  30308  disji2f  30340  disjif2  30344  disjxpin  30351  disjunsn  30357  preiman0  30469  cycpmco2f1  30816  tocyccntz  30836  isufd  31071  dimkerim  31111  prsss  31269  carsgclctunlem1  31685  carsgclctunlem2  31687  carsgclctunlem3  31688  ballotlemfval  31857  signsplypnf  31930  ftc2re  31979  fsum2dsub  31988  bnj1326  32408  f1resfz0f1d  32471  pthhashvtx  32487  satfv1  32723  satefv  32774  mvrsval  32865  msrfval  32897  mthmpps  32942  dfpo2  33104  elima4  33132  topbnd  33785  opnbnd  33786  cldbnd  33787  neibastop1  33820  neibastop2lem  33821  neibastop2  33822  neibastop3  33823  neifg  33832  bj-ismoored  34522  csbpredg  34743  pibt2  34834  poimirlem3  35060  mblfinlem2  35095  ftc1anclem6  35135  heiborlem3  35251  xrneq2  35792  elrefrels2  35917  refreleq  35920  elcnvrefrels2  35930  pmodN  37146  polvalN  37201  polatN  37227  trnsetN  37452  djavalN  38431  dihmeetbclemN  38600  dihmeetlem11N  38613  djhval  38694  lclkrlem2e  38807  lcfrlem23  38861  lcdlss2N  38916  metakunt18  39367  metakunt20  39369  elrfi  39635  elrfirn  39636  elrfirn2  39637  eldioph2lem1  39701  conrel2d  40365  ntrkbimka  40741  ntrk0kbimka  40742  isotone2  40752  ntrclskb  40772  ntrclsk3  40773  ntrclsk13  40774  clsneibex  40805  neicvgbex  40815  inabs3  41690  disjiun2  41692  fresin2  41796  lptioo2  42273  lptioo1  42274  limsupvaluz  42350  cncfuni  42528  fourierdlem48  42796  fourierdlem49  42797  fourierdlem93  42841  qndenserrnbllem  42936  nnfoctbdjlem  43094  carageniuncllem1  43160  carageniuncllem2  43161  hoiqssbllem3  43263  smflimlem3  43406  smflim  43410