Theorem ineq2d 3776

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

Syntax hints:   → wi 4   = wceq 1475   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  disjpr2OLD  4195  rint0  4452  riin0  4530  disji2  4569  disjprg  4578  disjxun  4581  xpriindi  5180  riinint  5303  reseq2  5312  resindm  5364  predep  5623  onfr  5680  fimacnvinrn  6256  fimacnvinrn2  6257  isofrlem  6490  isoselem  6491  oev2  7490  domss2  8004  funsnfsupp  8182  kmlem11  8865  fpwwe2cbv  9331  fpwwe2lem3  9334  fpwwe2lem8  9338  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  fz1isolem  13102  limsupgle  14056  fsumm1  14324  incexclem  14407  bitsinv1  15002  bitsinvp1  15009  sadcadd  15018  sadadd2  15020  smumullem  15052  ressbas  15757  ressress  15765  restval  15910  ismred2  16086  resscatc  16578  cnvps  17035  cntziinsn  17590  lsmdisj3r  17922  lsmdisj3b  17926  gsummptfzsplitl  18156  dmdprd  18220  subgdmdprd  18256  pgpfaclem1  18303  subrgpropd  18637  crng2idl  19060  obselocv  19891  basis1  20565  baspartn  20569  eltg  20572  tgdom  20593  indistopon  20615  ntrval  20650  clslp  20762  resttopon2  20782  restopnb  20789  paste  20908  nrmsep3  20969  imacmp  21010  cmpsub  21013  bwth  21023  llyi  21087  nllyi  21088  cldllycmp  21108  kgencmp2  21159  ptbasfi  21194  kqdisj  21345  kqcldsat  21346  trfbas2  21457  filss  21467  elfg  21485  flimclslem  21598  fcfneii  21651  tsmsfbas  21741  restutopopn  21852  ressxms  22140  restmetu  22185  qtopbaslem  22372  pi1addf  22655  pi1addval  22656  shftmbl  23113  voliunlem1  23125  voliunlem2  23126  uniioombllem2  23157  uniioombllem4  23160  uniioombllem6  23162  volsup2  23179  volcn  23180  volivth  23181  itg1climres  23287  limciun  23464  dvres3a  23484  ig1pval  23736  2pthlem2  26126  frgrancvvdeqlem4  26560  omlsi  27647  pjoml  27679  chdmj3  27774  chdmj4  27775  ledi  27783  cmbr  27827  cmbr3  27851  pjoml3  27855  fh1  27861  fh2  27862  dmdbr  28542  dmdmd  28543  dmdbr5  28551  dmdsl3  28558  chirredlem2  28634  chirredlem3  28635  dmdbr6ati  28666  disji2f  28772  disjif2  28776  disjxpin  28783  disjunsn  28789  prsss  29290  carsgclctunlem1  29706  carsgclctunlem2  29708  carsgclctunlem3  29709  ballotlemfval  29878  signsplypnf  29953  bnj1326  30348  mvrsval  30656  msrfval  30688  mthmpps  30733  dfpo2  30898  elima4  30924  topbnd  31489  opnbnd  31490  cldbnd  31491  neibastop1  31524  neibastop2lem  31525  neibastop2  31526  neibastop3  31527  neifg  31536  bj-diagval  32267  csbpredg  32348  poimirlem3  32582  mblfinlem2  32617  ftc1anclem6  32660  heiborlem3  32782  pmodN  34154  polvalN  34209  polatN  34235  trnsetN  34461  djavalN  35442  dihmeetbclemN  35611  dihmeetlem11N  35624  djhval  35705  lclkrlem2e  35818  lcfrlem23  35872  lcdlss2N  35927  elrfi  36275  elrfirn  36276  elrfirn2  36277  eldioph2lem1  36341  conrel2d  36975  ntrkbimka  37356  ntrk0kbimka  37357  isotone2  37367  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  clsneibex  37420  neicvgbex  37430  csbresgOLD  38077  inabs3  38249  disjiun2  38251  fresin2  38347  lptioo2  38698  lptioo1  38699  cncfuni  38772  fourierdlem48  39047  fourierdlem49  39048  fourierdlem93  39092  qndenserrnbllem  39190  nnfoctbdjlem  39348  carageniuncllem1  39411  carageniuncllem2  39412  hoiqssbllem3  39514  smflimlem3  39659  smflim  39663  resisresindm  40320  p1evtxdeqlem  40728  pthdlem2  40974  eupthp1  41384  frgrncvvdeqlem4  41472