Theorem ineq2d 4227

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

Syntax hints:   → wi 4   = wceq 1536   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-in 3969

This theorem is referenced by:  rint0  4992  riin0  5086  disji2  5131  disjprg  5143  disjxun  5145  xpriindi  5849  riinint  5984  reseq2  5994  resindm  6049  dfpo2  6317  csbpredg  6328  predep  6352  predprc  6360  predres  6361  onfr  6424  fimacnvinrn  7090  fimacnvinrn2  7091  isofrlem  7359  isoselem  7360  oev2  8559  domss2  9174  funsnfsupp  9429  kmlem11  10198  fpwwe2cbv  10667  fpwwe2lem3  10670  fpwwe2lem7  10674  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  fz1isolem  14496  limsupgle  15509  fsumm1  15783  incexclem  15868  bitsinv1  16475  bitsinvp1  16482  sadcadd  16491  sadadd2  16493  smumullem  16525  ressbas  17279  ressbasOLD  17280  ressress  17293  restval  17472  ismred2  17647  cat1lem  18149  resscatc  18162  cnvps  18635  cntziinsn  19367  lsmdisj3r  19718  lsmdisj3b  19722  gsummptfzsplitl  19965  dmdprd  20032  subgdmdprd  20068  pgpfaclem1  20115  subrngpropd  20584  subrgpropd  20624  crng2idl  21308  obselocv  21765  basis1  22972  baspartn  22976  eltg  22979  tgdom  23000  indistopon  23023  ntrval  23059  clslp  23171  resttopon2  23191  restopnb  23198  paste  23317  nrmsep3  23378  imacmp  23420  cmpsub  23423  bwth  23433  llyi  23497  nllyi  23498  cldllycmp  23518  kgencmp2  23569  ptbasfi  23604  kqdisj  23755  kqcldsat  23756  trfbas2  23866  filss  23876  elfg  23894  flimclslem  24007  fcfneii  24060  tsmsfbas  24151  restutopopn  24262  ressxms  24553  restmetu  24598  qtopbaslem  24794  pi1addf  25093  pi1addval  25094  shftmbl  25586  voliunlem1  25598  voliunlem2  25599  uniioombllem2  25631  uniioombllem4  25634  uniioombllem6  25636  volsup2  25653  volcn  25654  volivth  25655  itg1climres  25763  limciun  25943  dvres3a  25963  ig1pval  26229  p1evtxdeqlem  29544  pthdlem2  29800  eupthp1  30244  omlsi  31432  pjoml  31464  chdmj3  31559  chdmj4  31560  ledi  31568  cmbr  31612  cmbr3  31636  pjoml3  31640  fh1  31646  fh2  31647  dmdbr  32327  dmdmd  32328  dmdbr5  32336  dmdsl3  32343  chirredlem2  32419  chirredlem3  32420  dmdbr6ati  32451  unidifsnne  32561  disji2f  32596  disjif2  32600  disjxpin  32607  disjunsn  32613  preiman0  32724  cycpmco2f1  33126  tocyccntz  33146  oppr2idl  33493  isufd  33547  resssra  33616  dimkerim  33654  prsss  33876  carsgclctunlem1  34298  carsgclctunlem2  34300  carsgclctunlem3  34301  ballotlemfval  34470  signsplypnf  34543  ftc2re  34591  fsum2dsub  34600  bnj1326  35018  f1resfz0f1d  35097  pthhashvtx  35111  satfv1  35347  satefv  35398  mvrsval  35489  msrfval  35521  mthmpps  35566  elima4  35756  topbnd  36306  opnbnd  36307  cldbnd  36308  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  neibastop3  36344  neifg  36353  bj-ismoored  37089  pibt2  37399  poimirlem3  37609  mblfinlem2  37644  ftc1anclem6  37684  heiborlem3  37799  cnvref4  38331  xrneq2  38361  disjressuc2  38369  elrefrels2  38499  refreleq  38502  elcnvrefrels2  38515  pmodN  39832  polvalN  39887  polatN  39913  trnsetN  40138  djavalN  41117  dihmeetbclemN  41286  dihmeetlem11N  41299  djhval  41380  lclkrlem2e  41493  lcfrlem23  41547  lcdlss2N  41602  metakunt18  42203  metakunt20  42205  elrfi  42681  elrfirn  42682  elrfirn2  42683  eldioph2lem1  42747  conrel2d  43653  ntrkbimka  44027  ntrk0kbimka  44028  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  clsneibex  44091  neicvgbex  44101  ismnushort  44296  inabs3  44995  disjiun2  44997  fresin2  45114  lptioo2  45586  lptioo1  45587  limsupvaluz  45663  cncfuni  45841  fourierdlem48  46109  fourierdlem49  46110  fourierdlem93  46154  qndenserrnbllem  46249  nnfoctbdjlem  46410  carageniuncllem1  46476  carageniuncllem2  46477  hoiqssbllem3  46579  smflimlem3  46728  smflim  46732  restclsseplem  48710