Theorem ineq2d 4220

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  rint0  4988  riin0  5082  disji2  5127  disjprg  5139  disjxun  5141  xpriindi  5847  riinint  5982  reseq2  5992  resindm  6048  dfpo2  6316  csbpredg  6327  predep  6351  predprc  6359  predres  6360  onfr  6423  fimacnvinrn  7091  fimacnvinrn2  7092  isofrlem  7360  isoselem  7361  oev2  8561  domss2  9176  funsnfsupp  9432  kmlem11  10201  fpwwe2cbv  10670  fpwwe2lem3  10673  fpwwe2lem7  10677  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  fz1isolem  14500  limsupgle  15513  fsumm1  15787  incexclem  15872  bitsinv1  16479  bitsinvp1  16486  sadcadd  16495  sadadd2  16497  smumullem  16529  ressbas  17280  ressbasOLD  17281  ressress  17293  restval  17471  ismred2  17646  cat1lem  18141  resscatc  18154  cnvps  18623  cntziinsn  19355  lsmdisj3r  19704  lsmdisj3b  19708  gsummptfzsplitl  19951  dmdprd  20018  subgdmdprd  20054  pgpfaclem1  20101  subrngpropd  20568  subrgpropd  20608  crng2idl  21291  obselocv  21748  basis1  22957  baspartn  22961  eltg  22964  tgdom  22985  indistopon  23008  ntrval  23044  clslp  23156  resttopon2  23176  restopnb  23183  paste  23302  nrmsep3  23363  imacmp  23405  cmpsub  23408  bwth  23418  llyi  23482  nllyi  23483  cldllycmp  23503  kgencmp2  23554  ptbasfi  23589  kqdisj  23740  kqcldsat  23741  trfbas2  23851  filss  23861  elfg  23879  flimclslem  23992  fcfneii  24045  tsmsfbas  24136  restutopopn  24247  ressxms  24538  restmetu  24583  qtopbaslem  24779  pi1addf  25080  pi1addval  25081  shftmbl  25573  voliunlem1  25585  voliunlem2  25586  uniioombllem2  25618  uniioombllem4  25621  uniioombllem6  25623  volsup2  25640  volcn  25641  volivth  25642  itg1climres  25749  limciun  25929  dvres3a  25949  ig1pval  26215  p1evtxdeqlem  29530  pthdlem2  29788  eupthp1  30235  omlsi  31423  pjoml  31455  chdmj3  31550  chdmj4  31551  ledi  31559  cmbr  31603  cmbr3  31627  pjoml3  31631  fh1  31637  fh2  31638  dmdbr  32318  dmdmd  32319  dmdbr5  32327  dmdsl3  32334  chirredlem2  32410  chirredlem3  32411  dmdbr6ati  32442  unidifsnne  32554  disji2f  32590  disjif2  32594  disjxpin  32601  disjunsn  32607  preiman0  32719  cycpmco2f1  33144  tocyccntz  33164  oppr2idl  33514  isufd  33568  resssra  33638  dimkerim  33678  prsss  33915  carsgclctunlem1  34319  carsgclctunlem2  34321  carsgclctunlem3  34322  ballotlemfval  34492  signsplypnf  34565  ftc2re  34613  fsum2dsub  34622  bnj1326  35040  f1resfz0f1d  35119  pthhashvtx  35133  satfv1  35368  satefv  35419  mvrsval  35510  msrfval  35542  mthmpps  35587  elima4  35776  topbnd  36325  opnbnd  36326  cldbnd  36327  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  neibastop3  36363  neifg  36372  bj-ismoored  37108  pibt2  37418  poimirlem3  37630  mblfinlem2  37665  ftc1anclem6  37705  heiborlem3  37820  cnvref4  38351  xrneq2  38381  disjressuc2  38389  elrefrels2  38519  refreleq  38522  elcnvrefrels2  38535  pmodN  39852  polvalN  39907  polatN  39933  trnsetN  40158  djavalN  41137  dihmeetbclemN  41306  dihmeetlem11N  41319  djhval  41400  lclkrlem2e  41513  lcfrlem23  41567  lcdlss2N  41622  metakunt18  42223  metakunt20  42225  elrfi  42705  elrfirn  42706  elrfirn2  42707  eldioph2lem1  42771  conrel2d  43677  ntrkbimka  44051  ntrk0kbimka  44052  isotone2  44062  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  clsneibex  44115  neicvgbex  44125  ismnushort  44320  relpfrlem  44974  inabs3  45061  disjiun2  45063  fresin2  45177  lptioo2  45646  lptioo1  45647  limsupvaluz  45723  cncfuni  45901  fourierdlem48  46169  fourierdlem49  46170  fourierdlem93  46214  qndenserrnbllem  46309  nnfoctbdjlem  46470  carageniuncllem1  46536  carageniuncllem2  46537  hoiqssbllem3  46639  smflimlem3  46788  smflim  46792  resinsnALT  48773  restclsseplem  48812