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 1541   ∩ cin 3900

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  rint0  4943  riin0  5037  disji2  5082  disjprg  5094  disjxun  5096  xpriindi  5785  riinint  5921  reseq2  5933  resindm  5989  dfpo2  6254  csbpredg  6265  predep  6288  predprc  6296  predres  6297  onfr  6356  fimacnvinrn  7016  fimacnvinrn2  7017  isofrlem  7286  isoselem  7287  oev2  8450  domss2  9064  funsnfsupp  9295  kmlem11  10071  fpwwe2cbv  10541  fpwwe2lem3  10544  fpwwe2lem7  10548  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  fz1isolem  14384  limsupgle  15400  fsumm1  15674  incexclem  15759  bitsinv1  16369  bitsinvp1  16376  sadcadd  16385  sadadd2  16387  smumullem  16419  ressbas  17163  ressress  17174  restval  17346  ismred2  17522  cat1lem  18020  resscatc  18033  cnvps  18501  cntziinsn  19266  lsmdisj3r  19615  lsmdisj3b  19619  gsummptfzsplitl  19862  dmdprd  19929  subgdmdprd  19965  pgpfaclem1  20012  subrngpropd  20501  subrgpropd  20541  crng2idl  21236  obselocv  21683  basis1  22894  baspartn  22898  eltg  22901  tgdom  22922  indistopon  22945  ntrval  22980  clslp  23092  resttopon2  23112  restopnb  23119  paste  23238  nrmsep3  23299  imacmp  23341  cmpsub  23344  bwth  23354  llyi  23418  nllyi  23419  cldllycmp  23439  kgencmp2  23490  ptbasfi  23525  kqdisj  23676  kqcldsat  23677  trfbas2  23787  filss  23797  elfg  23815  flimclslem  23928  fcfneii  23981  tsmsfbas  24072  restutopopn  24182  ressxms  24469  restmetu  24514  qtopbaslem  24702  pi1addf  25003  pi1addval  25004  shftmbl  25495  voliunlem1  25507  voliunlem2  25508  uniioombllem2  25540  uniioombllem4  25543  uniioombllem6  25545  volsup2  25562  volcn  25563  volivth  25564  itg1climres  25671  limciun  25851  dvres3a  25871  ig1pval  26137  p1evtxdeqlem  29586  pthdlem2  29841  eupthp1  30291  omlsi  31479  pjoml  31511  chdmj3  31606  chdmj4  31607  ledi  31615  cmbr  31659  cmbr3  31683  pjoml3  31687  fh1  31693  fh2  31694  dmdbr  32374  dmdmd  32375  dmdbr5  32383  dmdsl3  32390  chirredlem2  32466  chirredlem3  32467  dmdbr6ati  32498  unidifsnne  32611  disji2f  32652  disjif2  32656  disjxpin  32663  disjunsn  32669  preiman0  32789  nn0diffz0  32874  cycpmco2f1  33206  tocyccntz  33226  oppr2idl  33567  isufd  33621  resssra  33743  dimkerim  33784  prsss  34073  carsgclctunlem1  34474  carsgclctunlem2  34476  carsgclctunlem3  34477  ballotlemfval  34647  signsplypnf  34707  ftc2re  34755  fsum2dsub  34764  bnj1326  35182  f1resfz0f1d  35308  pthhashvtx  35322  satfv1  35557  satefv  35608  mvrsval  35699  msrfval  35731  mthmpps  35776  elima4  35970  topbnd  36518  opnbnd  36519  cldbnd  36520  neibastop1  36553  neibastop2lem  36554  neibastop2  36555  neibastop3  36556  neifg  36565  bj-ismoored  37312  pibt2  37622  poimirlem3  37824  mblfinlem2  37859  ftc1anclem6  37899  heiborlem3  38014  cnvref4  38543  xrneq2  38584  disjressuc2  38596  elrefrels2  38771  refreleq  38774  elcnvrefrels2  38787  pmodN  40110  polvalN  40165  polatN  40191  trnsetN  40416  djavalN  41395  dihmeetbclemN  41564  dihmeetlem11N  41577  djhval  41658  lclkrlem2e  41771  lcfrlem23  41825  lcdlss2N  41880  elrfi  42936  elrfirn  42937  elrfirn2  42938  eldioph2lem1  43002  conrel2d  43905  ntrkbimka  44279  ntrk0kbimka  44280  isotone2  44290  ntrclskb  44310  ntrclsk3  44311  ntrclsk13  44312  clsneibex  44343  neicvgbex  44353  ismnushort  44542  relpfrlem  45194  inabs3  45301  disjiun2  45303  fresin2  45416  lptioo2  45877  lptioo1  45878  limsupvaluz  45952  cncfuni  46130  fourierdlem48  46398  fourierdlem49  46399  fourierdlem93  46443  qndenserrnbllem  46538  nnfoctbdjlem  46699  carageniuncllem1  46765  carageniuncllem2  46766  hoiqssbllem3  46868  smflimlem3  47017  smflim  47021  resinsnALT  49118  restclsseplem  49160