Theorem ineq2d 4171

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3902

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-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-in 3910

This theorem is referenced by:  rint0  4938  riin0  5031  disji2  5076  disjprg  5088  disjxun  5090  xpriindi  5779  riinint  5913  reseq2  5925  resindm  5981  dfpo2  6244  csbpredg  6255  predep  6278  predprc  6286  predres  6287  onfr  6346  fimacnvinrn  7005  fimacnvinrn2  7006  isofrlem  7277  isoselem  7278  oev2  8441  domss2  9053  funsnfsupp  9282  kmlem11  10055  fpwwe2cbv  10524  fpwwe2lem3  10527  fpwwe2lem7  10531  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  fz1isolem  14368  limsupgle  15384  fsumm1  15658  incexclem  15743  bitsinv1  16353  bitsinvp1  16360  sadcadd  16369  sadadd2  16371  smumullem  16403  ressbas  17147  ressress  17158  restval  17330  ismred2  17505  cat1lem  18003  resscatc  18016  cnvps  18484  cntziinsn  19216  lsmdisj3r  19565  lsmdisj3b  19569  gsummptfzsplitl  19812  dmdprd  19879  subgdmdprd  19915  pgpfaclem1  19962  subrngpropd  20453  subrgpropd  20493  crng2idl  21188  obselocv  21635  basis1  22835  baspartn  22839  eltg  22842  tgdom  22863  indistopon  22886  ntrval  22921  clslp  23033  resttopon2  23053  restopnb  23060  paste  23179  nrmsep3  23240  imacmp  23282  cmpsub  23285  bwth  23295  llyi  23359  nllyi  23360  cldllycmp  23380  kgencmp2  23431  ptbasfi  23466  kqdisj  23617  kqcldsat  23618  trfbas2  23728  filss  23738  elfg  23756  flimclslem  23869  fcfneii  23922  tsmsfbas  24013  restutopopn  24124  ressxms  24411  restmetu  24456  qtopbaslem  24644  pi1addf  24945  pi1addval  24946  shftmbl  25437  voliunlem1  25449  voliunlem2  25450  uniioombllem2  25482  uniioombllem4  25485  uniioombllem6  25487  volsup2  25504  volcn  25505  volivth  25506  itg1climres  25613  limciun  25793  dvres3a  25813  ig1pval  26079  p1evtxdeqlem  29458  pthdlem2  29713  eupthp1  30160  omlsi  31348  pjoml  31380  chdmj3  31475  chdmj4  31476  ledi  31484  cmbr  31528  cmbr3  31552  pjoml3  31556  fh1  31562  fh2  31563  dmdbr  32243  dmdmd  32244  dmdbr5  32252  dmdsl3  32259  chirredlem2  32335  chirredlem3  32336  dmdbr6ati  32367  unidifsnne  32480  disji2f  32521  disjif2  32525  disjxpin  32532  disjunsn  32538  preiman0  32652  cycpmco2f1  33066  tocyccntz  33086  oppr2idl  33423  isufd  33477  resssra  33553  dimkerim  33594  prsss  33883  carsgclctunlem1  34285  carsgclctunlem2  34287  carsgclctunlem3  34288  ballotlemfval  34458  signsplypnf  34518  ftc2re  34566  fsum2dsub  34575  bnj1326  34993  f1resfz0f1d  35087  pthhashvtx  35101  satfv1  35336  satefv  35387  mvrsval  35478  msrfval  35510  mthmpps  35555  elima4  35749  topbnd  36298  opnbnd  36299  cldbnd  36300  neibastop1  36333  neibastop2lem  36334  neibastop2  36335  neibastop3  36336  neifg  36345  bj-ismoored  37081  pibt2  37391  poimirlem3  37603  mblfinlem2  37638  ftc1anclem6  37678  heiborlem3  37793  cnvref4  38318  xrneq2  38352  disjressuc2  38360  elrefrels2  38495  refreleq  38498  elcnvrefrels2  38511  pmodN  39829  polvalN  39884  polatN  39910  trnsetN  40135  djavalN  41114  dihmeetbclemN  41283  dihmeetlem11N  41296  djhval  41377  lclkrlem2e  41490  lcfrlem23  41544  lcdlss2N  41599  elrfi  42667  elrfirn  42668  elrfirn2  42669  eldioph2lem1  42733  conrel2d  43637  ntrkbimka  44011  ntrk0kbimka  44012  isotone2  44022  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  clsneibex  44075  neicvgbex  44085  ismnushort  44274  relpfrlem  44927  inabs3  45034  disjiun2  45036  fresin2  45150  lptioo2  45612  lptioo1  45613  limsupvaluz  45689  cncfuni  45867  fourierdlem48  46135  fourierdlem49  46136  fourierdlem93  46180  qndenserrnbllem  46275  nnfoctbdjlem  46436  carageniuncllem1  46502  carageniuncllem2  46503  hoiqssbllem3  46605  smflimlem3  46754  smflim  46758  resinsnALT  48857  restclsseplem  48899