Theorem ineq2d 4118

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-in 3866

This theorem is referenced by:  rint0  4881  riin0  4970  disji2  5015  disjprgw  5028  disjprg  5029  disjxun  5031  xpriindi  5677  riinint  5810  reseq2  5819  resindm  5873  predep  6153  onfr  6209  fimacnvinrn  6832  fimacnvinrn2  6833  isofrlem  7088  isoselem  7089  oev2  8159  domss2  8698  funsnfsupp  8883  kmlem11  9613  fpwwe2cbv  10083  fpwwe2lem3  10086  fpwwe2lem7  10090  fpwwe2lem11  10094  fpwwe2lem12  10095  fpwwe2  10096  fz1isolem  13864  limsupgle  14875  fsumm1  15147  incexclem  15232  bitsinv1  15834  bitsinvp1  15841  sadcadd  15850  sadadd2  15852  smumullem  15884  ressbas  16605  ressress  16613  restval  16751  ismred2  16925  resscatc  17424  cnvps  17881  cntziinsn  18525  lsmdisj3r  18872  lsmdisj3b  18876  gsummptfzsplitl  19114  dmdprd  19181  subgdmdprd  19217  pgpfaclem1  19264  subrgpropd  19631  crng2idl  20073  obselocv  20486  basis1  21643  baspartn  21647  eltg  21650  tgdom  21671  indistopon  21694  ntrval  21729  clslp  21841  resttopon2  21861  restopnb  21868  paste  21987  nrmsep3  22048  imacmp  22090  cmpsub  22093  bwth  22103  llyi  22167  nllyi  22168  cldllycmp  22188  kgencmp2  22239  ptbasfi  22274  kqdisj  22425  kqcldsat  22426  trfbas2  22536  filss  22546  elfg  22564  flimclslem  22677  fcfneii  22730  tsmsfbas  22821  restutopopn  22932  ressxms  23220  restmetu  23265  qtopbaslem  23453  pi1addf  23741  pi1addval  23742  shftmbl  24231  voliunlem1  24243  voliunlem2  24244  uniioombllem2  24276  uniioombllem4  24279  uniioombllem6  24281  volsup2  24298  volcn  24299  volivth  24300  itg1climres  24407  limciun  24586  dvres3a  24606  ig1pval  24865  p1evtxdeqlem  27394  pthdlem2  27649  eupthp1  28093  omlsi  29279  pjoml  29311  chdmj3  29406  chdmj4  29407  ledi  29415  cmbr  29459  cmbr3  29483  pjoml3  29487  fh1  29493  fh2  29494  dmdbr  30174  dmdmd  30175  dmdbr5  30183  dmdsl3  30190  chirredlem2  30266  chirredlem3  30267  dmdbr6ati  30298  unidifsnne  30399  disji2f  30431  disjif2  30435  disjxpin  30442  disjunsn  30448  preiman0  30559  cycpmco2f1  30910  tocyccntz  30930  isufd  31177  dimkerim  31222  prsss  31380  carsgclctunlem1  31796  carsgclctunlem2  31798  carsgclctunlem3  31799  ballotlemfval  31968  signsplypnf  32041  ftc2re  32090  fsum2dsub  32099  bnj1326  32519  f1resfz0f1d  32582  pthhashvtx  32598  satfv1  32834  satefv  32885  mvrsval  32976  msrfval  33008  mthmpps  33053  dfpo2  33231  elima4  33259  topbnd  34055  opnbnd  34056  cldbnd  34057  neibastop1  34090  neibastop2lem  34091  neibastop2  34092  neibastop3  34093  neifg  34102  bj-ismoored  34795  csbpredg  35016  pibt2  35107  poimirlem3  35333  mblfinlem2  35368  ftc1anclem6  35408  heiborlem3  35524  xrneq2  36065  elrefrels2  36190  refreleq  36193  elcnvrefrels2  36203  pmodN  37419  polvalN  37474  polatN  37500  trnsetN  37725  djavalN  38704  dihmeetbclemN  38873  dihmeetlem11N  38886  djhval  38967  lclkrlem2e  39080  lcfrlem23  39134  lcdlss2N  39189  metakunt18  39657  metakunt20  39659  elrfi  40001  elrfirn  40002  elrfirn2  40003  eldioph2lem1  40067  conrel2d  40731  ntrkbimka  41107  ntrk0kbimka  41108  isotone2  41118  ntrclskb  41138  ntrclsk3  41139  ntrclsk13  41140  clsneibex  41171  neicvgbex  41181  inabs3  42056  disjiun2  42058  fresin2  42160  lptioo2  42632  lptioo1  42633  limsupvaluz  42709  cncfuni  42887  fourierdlem48  43155  fourierdlem49  43156  fourierdlem93  43200  qndenserrnbllem  43295  nnfoctbdjlem  43453  carageniuncllem1  43519  carageniuncllem2  43520  hoiqssbllem3  43622  smflimlem3  43765  smflim  43769