Theorem ineq2d 4143

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  rint0  4918  riin0  5007  disji2  5052  disjprgw  5065  disjprg  5066  disjxun  5068  xpriindi  5734  riinint  5866  reseq2  5875  resindm  5929  dfpo2  6188  csbpredg  6197  predep  6222  onfr  6290  fimacnvinrn  6931  fimacnvinrn2  6932  isofrlem  7191  isoselem  7192  oev2  8315  domss2  8872  funsnfsupp  9082  kmlem11  9847  fpwwe2cbv  10317  fpwwe2lem3  10320  fpwwe2lem7  10324  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  fz1isolem  14103  limsupgle  15114  fsumm1  15391  incexclem  15476  bitsinv1  16077  bitsinvp1  16084  sadcadd  16093  sadadd2  16095  smumullem  16127  ressbas  16873  ressbasOLD  16874  ressress  16884  restval  17054  ismred2  17229  cat1lem  17727  resscatc  17740  cnvps  18211  cntziinsn  18856  lsmdisj3r  19207  lsmdisj3b  19211  gsummptfzsplitl  19449  dmdprd  19516  subgdmdprd  19552  pgpfaclem1  19599  subrgpropd  19974  crng2idl  20423  obselocv  20845  basis1  22008  baspartn  22012  eltg  22015  tgdom  22036  indistopon  22059  ntrval  22095  clslp  22207  resttopon2  22227  restopnb  22234  paste  22353  nrmsep3  22414  imacmp  22456  cmpsub  22459  bwth  22469  llyi  22533  nllyi  22534  cldllycmp  22554  kgencmp2  22605  ptbasfi  22640  kqdisj  22791  kqcldsat  22792  trfbas2  22902  filss  22912  elfg  22930  flimclslem  23043  fcfneii  23096  tsmsfbas  23187  restutopopn  23298  ressxms  23587  restmetu  23632  qtopbaslem  23828  pi1addf  24116  pi1addval  24117  shftmbl  24607  voliunlem1  24619  voliunlem2  24620  uniioombllem2  24652  uniioombllem4  24655  uniioombllem6  24657  volsup2  24674  volcn  24675  volivth  24676  itg1climres  24784  limciun  24963  dvres3a  24983  ig1pval  25242  p1evtxdeqlem  27782  pthdlem2  28037  eupthp1  28481  omlsi  29667  pjoml  29699  chdmj3  29794  chdmj4  29795  ledi  29803  cmbr  29847  cmbr3  29871  pjoml3  29875  fh1  29881  fh2  29882  dmdbr  30562  dmdmd  30563  dmdbr5  30571  dmdsl3  30578  chirredlem2  30654  chirredlem3  30655  dmdbr6ati  30686  unidifsnne  30785  disji2f  30817  disjif2  30821  disjxpin  30828  disjunsn  30834  preiman0  30944  cycpmco2f1  31293  tocyccntz  31313  isufd  31565  dimkerim  31610  prsss  31768  carsgclctunlem1  32184  carsgclctunlem2  32186  carsgclctunlem3  32187  ballotlemfval  32356  signsplypnf  32429  ftc2re  32478  fsum2dsub  32487  bnj1326  32906  f1resfz0f1d  32972  pthhashvtx  32989  satfv1  33225  satefv  33276  mvrsval  33367  msrfval  33399  mthmpps  33444  elima4  33656  topbnd  34440  opnbnd  34441  cldbnd  34442  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  neibastop3  34478  neifg  34487  bj-ismoored  35205  pibt2  35515  poimirlem3  35707  mblfinlem2  35742  ftc1anclem6  35782  heiborlem3  35898  xrneq2  36437  elrefrels2  36562  refreleq  36565  elcnvrefrels2  36575  pmodN  37791  polvalN  37846  polatN  37872  trnsetN  38097  djavalN  39076  dihmeetbclemN  39245  dihmeetlem11N  39258  djhval  39339  lclkrlem2e  39452  lcfrlem23  39506  lcdlss2N  39561  metakunt18  40070  metakunt20  40072  elrfi  40432  elrfirn  40433  elrfirn2  40434  eldioph2lem1  40498  conrel2d  41161  ntrkbimka  41537  ntrk0kbimka  41538  isotone2  41548  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  clsneibex  41601  neicvgbex  41611  ismnushort  41808  inabs3  42493  disjiun2  42495  fresin2  42597  lptioo2  43062  lptioo1  43063  limsupvaluz  43139  cncfuni  43317  fourierdlem48  43585  fourierdlem49  43586  fourierdlem93  43630  qndenserrnbllem  43725  nnfoctbdjlem  43883  carageniuncllem1  43949  carageniuncllem2  43950  hoiqssbllem3  44052  smflimlem3  44195  smflim  44199  restclsseplem  46096