Theorem ineq2d 4172

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 4166	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∩ 𝐴) = (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   = wceq 1560   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-in 3911

This theorem is referenced by:  rint0  4946  riin0  5039  disji2  5084  disjprg  5096  disjxun  5098  xpriindi  5808  riinint  5948  reseq2  5960  resindmOLD  6017  dfpo2  6283  csbpredg  6294  predep  6317  predprc  6325  predres  6326  onfr  6385  fimacnvinrn  7052  fimacnvinrn2  7053  isofrlem  7324  isoselem  7325  oev2  8492  domss2  9108  funsnfsupp  9338  kmlem11  10117  fpwwe2cbv  10588  fpwwe2lem3  10591  fpwwe2lem7  10595  fpwwe2lem11  10599  fpwwe2lem12  10600  fpwwe2  10601  fz1isolem  14474  limsupgle  15504  fsumm1  15778  incexclem  15866  bitsinv1  16476  bitsinvp1  16483  sadcadd  16492  sadadd2  16494  smumullem  16526  ressbas  17272  ressress  17283  restval  17455  ismred2  17631  cat1lem  18129  resscatc  18142  cnvps  18610  cntziinsn  19377  lsmdisj3r  19726  lsmdisj3b  19730  gsummptfzsplitl  19973  dmdprd  20040  subgdmdprd  20076  pgpfaclem1  20123  subrngpropd  20614  subrgpropd  20654  crng2idl  21348  obselocv  21777  basis1  23007  baspartn  23011  eltg  23014  tgdom  23035  indistopon  23058  ntrval  23093  clslp  23205  resttopon2  23225  restopnb  23232  paste  23351  nrmsep3  23412  imacmp  23454  cmpsub  23457  bwth  23467  llyi  23531  nllyi  23532  cldllycmp  23552  kgencmp2  23603  ptbasfi  23638  kqdisj  23789  kqcldsat  23790  trfbas2  23900  filss  23910  elfg  23928  flimclslem  24041  fcfneii  24094  tsmsfbas  24185  restutopopn  24295  ressxms  24582  restmetu  24627  qtopbaslem  24815  pi1addf  25106  pi1addval  25107  shftmbl  25597  voliunlem1  25609  voliunlem2  25610  uniioombllem2  25642  uniioombllem4  25645  uniioombllem6  25647  volsup2  25664  volcn  25665  volivth  25666  itg1climres  25773  limciun  25953  dvres3a  25973  ig1pval  26233  p1evtxdeqlem  29710  pthdlem2  29965  eupthp1  30415  omlsi  31604  pjoml  31636  chdmj3  31731  chdmj4  31732  ledi  31740  cmbr  31784  cmbr3  31808  pjoml3  31812  fh1  31818  fh2  31819  dmdbr  32499  dmdmd  32500  dmdbr5  32508  dmdsl3  32515  chirredlem2  32591  chirredlem3  32592  dmdbr6ati  32623  unidifsnne  32732  disji2f  32774  disjif2  32778  disjxpin  32785  disjunsn  32791  preiman0  32909  nn0diffz0  32993  cycpmco2f1  33301  tocyccntz  33321  oppr2idl  33671  isufd  33733  resssra  33881  dimkerim  33921  prsss  34210  carsgclctunlem1  34611  carsgclctunlem2  34613  carsgclctunlem3  34614  ballotlemfval  34784  signsplypnf  34841  ftc2re  34889  fsum2dsub  34898  bnj1326  35318  f1resfz0f1d  35461  pthhashvtx  35475  satfv1  35710  satefv  35761  mvrsval  35852  msrfval  35884  mthmpps  35929  elima4  36123  topbnd  36681  opnbnd  36682  cldbnd  36683  neibastop1  36716  neibastop2lem  36717  neibastop2  36718  neibastop3  36719  neifg  36728  dfttc4lem2  36886  bj-ismoored  37594  pibt2  37908  poimirlem3  38119  mblfinlem2  38154  ftc1anclem6  38194  heiborlem3  38309  cnvref4  38846  xrneq2  38895  disjressuc2  38907  elrefrels2  39094  refreleq  39097  elcnvrefrels2  39110  pmodN  40471  polvalN  40526  polatN  40552  trnsetN  40777  djavalN  41756  dihmeetbclemN  41925  dihmeetlem11N  41938  djhval  42019  lclkrlem2e  42132  lcfrlem23  42186  lcdlss2N  42241  elrfi  43272  elrfirn  43273  elrfirn2  43274  eldioph2lem1  43338  conrel2d  44237  ntrkbimka  44611  ntrk0kbimka  44612  isotone2  44622  ntrclskb  44642  ntrclsk3  44643  ntrclsk13  44644  clsneibex  44675  neicvgbex  44685  ismnushort  44874  relpfrlem  45526  inabs3  45633  disjiun2  45635  fresin2  45747  lptioo2  46204  lptioo1  46205  limsupvaluz  46279  cncfuni  46457  fourierdlem48  46725  fourierdlem49  46726  fourierdlem93  46770  qndenserrnbllem  46865  nnfoctbdjlem  47026  carageniuncllem1  47092  carageniuncllem2  47093  hoiqssbllem3  47195  smflimlem3  47344  smflim  47348  resinsnALT  49491  restclsseplem  49533