Theorem ineq2d 4149

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

Syntax hints:   → wi 4   = wceq 1547   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  rint0  4918  riin0  5011  disji2  5056  disjprg  5068  disjxun  5070  xpriindi  5778  riinint  5914  reseq2  5926  resindm  5982  dfpo2  6247  csbpredg  6258  predep  6281  predprc  6289  predres  6290  onfr  6349  fimacnvinrn  7012  fimacnvinrn2  7013  isofrlem  7284  isoselem  7285  oev2  8448  domss2  9064  funsnfsupp  9295  kmlem11  10074  fpwwe2cbv  10544  fpwwe2lem3  10547  fpwwe2lem7  10551  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  fz1isolem  14414  limsupgle  15430  fsumm1  15704  incexclem  15792  bitsinv1  16402  bitsinvp1  16409  sadcadd  16418  sadadd2  16420  smumullem  16452  ressbas  17197  ressress  17208  restval  17380  ismred2  17556  cat1lem  18054  resscatc  18067  cnvps  18535  cntziinsn  19303  lsmdisj3r  19652  lsmdisj3b  19656  gsummptfzsplitl  19899  dmdprd  19966  subgdmdprd  20002  pgpfaclem1  20049  subrngpropd  20540  subrgpropd  20580  crng2idl  21274  obselocv  21703  basis1  22933  baspartn  22937  eltg  22940  tgdom  22961  indistopon  22984  ntrval  23019  clslp  23131  resttopon2  23151  restopnb  23158  paste  23277  nrmsep3  23338  imacmp  23380  cmpsub  23383  bwth  23393  llyi  23457  nllyi  23458  cldllycmp  23478  kgencmp2  23529  ptbasfi  23564  kqdisj  23715  kqcldsat  23716  trfbas2  23826  filss  23836  elfg  23854  flimclslem  23967  fcfneii  24020  tsmsfbas  24111  restutopopn  24221  ressxms  24508  restmetu  24553  qtopbaslem  24741  pi1addf  25032  pi1addval  25033  shftmbl  25523  voliunlem1  25535  voliunlem2  25536  uniioombllem2  25568  uniioombllem4  25571  uniioombllem6  25573  volsup2  25590  volcn  25591  volivth  25592  itg1climres  25699  limciun  25879  dvres3a  25899  ig1pval  26159  p1evtxdeqlem  29599  pthdlem2  29854  eupthp1  30304  omlsi  31493  pjoml  31525  chdmj3  31620  chdmj4  31621  ledi  31629  cmbr  31673  cmbr3  31697  pjoml3  31701  fh1  31707  fh2  31708  dmdbr  32388  dmdmd  32389  dmdbr5  32397  dmdsl3  32404  chirredlem2  32480  chirredlem3  32481  dmdbr6ati  32512  unidifsnne  32624  disji2f  32666  disjif2  32670  disjxpin  32677  disjunsn  32683  preiman0  32802  nn0diffz0  32886  cycpmco2f1  33205  tocyccntz  33225  oppr2idl  33569  isufd  33623  resssra  33771  dimkerim  33811  prsss  34100  carsgclctunlem1  34501  carsgclctunlem2  34503  carsgclctunlem3  34504  ballotlemfval  34674  signsplypnf  34734  ftc2re  34782  fsum2dsub  34791  bnj1326  35208  f1resfz0f1d  35342  pthhashvtx  35356  satfv1  35591  satefv  35642  mvrsval  35733  msrfval  35765  mthmpps  35810  elima4  36004  topbnd  36552  opnbnd  36553  cldbnd  36554  neibastop1  36587  neibastop2lem  36588  neibastop2  36589  neibastop3  36590  neifg  36599  dfttc4lem2  36757  bj-ismoored  37465  pibt2  37779  poimirlem3  37990  mblfinlem2  38025  ftc1anclem6  38065  heiborlem3  38180  cnvref4  38717  xrneq2  38766  disjressuc2  38778  elrefrels2  38965  refreleq  38968  elcnvrefrels2  38981  pmodN  40342  polvalN  40397  polatN  40423  trnsetN  40648  djavalN  41627  dihmeetbclemN  41796  dihmeetlem11N  41809  djhval  41890  lclkrlem2e  42003  lcfrlem23  42057  lcdlss2N  42112  elrfi  43143  elrfirn  43144  elrfirn2  43145  eldioph2lem1  43209  conrel2d  44108  ntrkbimka  44482  ntrk0kbimka  44483  isotone2  44493  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  clsneibex  44546  neicvgbex  44556  ismnushort  44745  relpfrlem  45397  inabs3  45504  disjiun2  45506  fresin2  45619  lptioo2  46076  lptioo1  46077  limsupvaluz  46151  cncfuni  46329  fourierdlem48  46597  fourierdlem49  46598  fourierdlem93  46642  qndenserrnbllem  46737  nnfoctbdjlem  46898  carageniuncllem1  46964  carageniuncllem2  46965  hoiqssbllem3  47067  smflimlem3  47216  smflim  47220  resinsnALT  49363  restclsseplem  49405