Theorem ineq2d 4212

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955

This theorem is referenced by:  rint0  4994  riin0  5085  disji2  5130  disjprgw  5143  disjprg  5144  disjxun  5146  xpriindi  5836  riinint  5967  reseq2  5976  resindm  6030  dfpo2  6295  csbpredg  6306  predep  6331  predprc  6339  predres  6340  onfr  6403  fimacnvinrn  7073  fimacnvinrn2  7074  isofrlem  7336  isoselem  7337  oev2  8522  domss2  9135  funsnfsupp  9386  kmlem11  10154  fpwwe2cbv  10624  fpwwe2lem3  10627  fpwwe2lem7  10631  fpwwe2lem11  10635  fpwwe2lem12  10636  fpwwe2  10637  fz1isolem  14421  limsupgle  15420  fsumm1  15696  incexclem  15781  bitsinv1  16382  bitsinvp1  16389  sadcadd  16398  sadadd2  16400  smumullem  16432  ressbas  17178  ressbasOLD  17179  ressress  17192  restval  17371  ismred2  17546  cat1lem  18045  resscatc  18058  cnvps  18530  cntziinsn  19200  lsmdisj3r  19553  lsmdisj3b  19557  gsummptfzsplitl  19800  dmdprd  19867  subgdmdprd  19903  pgpfaclem1  19950  subrgpropd  20354  crng2idl  20876  obselocv  21282  basis1  22452  baspartn  22456  eltg  22459  tgdom  22480  indistopon  22503  ntrval  22539  clslp  22651  resttopon2  22671  restopnb  22678  paste  22797  nrmsep3  22858  imacmp  22900  cmpsub  22903  bwth  22913  llyi  22977  nllyi  22978  cldllycmp  22998  kgencmp2  23049  ptbasfi  23084  kqdisj  23235  kqcldsat  23236  trfbas2  23346  filss  23356  elfg  23374  flimclslem  23487  fcfneii  23540  tsmsfbas  23631  restutopopn  23742  ressxms  24033  restmetu  24078  qtopbaslem  24274  pi1addf  24562  pi1addval  24563  shftmbl  25054  voliunlem1  25066  voliunlem2  25067  uniioombllem2  25099  uniioombllem4  25102  uniioombllem6  25104  volsup2  25121  volcn  25122  volivth  25123  itg1climres  25231  limciun  25410  dvres3a  25430  ig1pval  25689  p1evtxdeqlem  28766  pthdlem2  29022  eupthp1  29466  omlsi  30652  pjoml  30684  chdmj3  30779  chdmj4  30780  ledi  30788  cmbr  30832  cmbr3  30856  pjoml3  30860  fh1  30866  fh2  30867  dmdbr  31547  dmdmd  31548  dmdbr5  31556  dmdsl3  31563  chirredlem2  31639  chirredlem3  31640  dmdbr6ati  31671  unidifsnne  31768  disji2f  31803  disjif2  31807  disjxpin  31814  disjunsn  31820  preiman0  31926  cycpmco2f1  32278  tocyccntz  32298  oppr2idl  32595  isufd  32627  dimkerim  32707  prsss  32891  carsgclctunlem1  33311  carsgclctunlem2  33313  carsgclctunlem3  33314  ballotlemfval  33483  signsplypnf  33556  ftc2re  33605  fsum2dsub  33614  bnj1326  34032  f1resfz0f1d  34098  pthhashvtx  34113  satfv1  34349  satefv  34400  mvrsval  34491  msrfval  34523  mthmpps  34568  elima4  34742  topbnd  35204  opnbnd  35205  cldbnd  35206  neibastop1  35239  neibastop2lem  35240  neibastop2  35241  neibastop3  35242  neifg  35251  bj-ismoored  35983  pibt2  36293  poimirlem3  36486  mblfinlem2  36521  ftc1anclem6  36561  heiborlem3  36676  cnvref4  37214  xrneq2  37245  disjressuc2  37253  elrefrels2  37383  refreleq  37386  elcnvrefrels2  37399  pmodN  38716  polvalN  38771  polatN  38797  trnsetN  39022  djavalN  40001  dihmeetbclemN  40170  dihmeetlem11N  40183  djhval  40264  lclkrlem2e  40377  lcfrlem23  40431  lcdlss2N  40486  metakunt18  40997  metakunt20  40999  elrfi  41422  elrfirn  41423  elrfirn2  41424  eldioph2lem1  41488  conrel2d  42405  ntrkbimka  42779  ntrk0kbimka  42780  isotone2  42790  ntrclskb  42810  ntrclsk3  42811  ntrclsk13  42812  clsneibex  42843  neicvgbex  42853  ismnushort  43050  inabs3  43733  disjiun2  43735  fresin2  43858  lptioo2  44337  lptioo1  44338  limsupvaluz  44414  cncfuni  44592  fourierdlem48  44860  fourierdlem49  44861  fourierdlem93  44905  qndenserrnbllem  45000  nnfoctbdjlem  45161  carageniuncllem1  45227  carageniuncllem2  45228  hoiqssbllem3  45330  smflimlem3  45479  smflim  45483  subrngpropd  46737  restclsseplem  47537