Theorem ineq2d 4181

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

Syntax hints:   → wi 4   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  rint0  4957  riin0  5052  disji2  5097  disjprg  5109  disjxun  5111  xpriindi  5823  riinint  5963  reseq2  5974  resindmOLD  6031  dfpo2  6298  csbpredg  6309  predep  6332  predprc  6340  predres  6341  onfr  6401  fimacnvinrn  7067  fimacnvinrn2  7068  isofrlem  7339  isoselem  7340  oev2  8507  domss2  9123  funsnfsupp  9351  kmlem11  10143  fpwwe2cbv  10614  fpwwe2lem3  10617  fpwwe2lem7  10621  fpwwe2lem11  10625  fpwwe2lem12  10626  fpwwe2  10627  fz1isolem  14497  limsupgle  15527  fsumm1  15801  incexclem  15889  bitsinv1  16499  bitsinvp1  16506  sadcadd  16515  sadadd2  16517  smumullem  16549  ressbas  17295  ressress  17306  restval  17478  ismred2  17654  cat1lem  18152  resscatc  18165  cnvps  18633  cntziinsn  19406  lsmdisj3r  19755  lsmdisj3b  19759  gsummptfzsplitl  20002  dmdprd  20069  subgdmdprd  20105  pgpfaclem1  20152  subrngpropd  20652  subrgpropd  20692  crng2idl  21390  obselocv  21846  basis1  23075  baspartn  23079  eltg  23082  tgdom  23103  indistopon  23126  ntrval  23161  clslp  23273  resttopon2  23293  restopnb  23300  paste  23419  nrmsep3  23480  imacmp  23522  cmpsub  23525  bwth  23535  llyi  23599  nllyi  23600  cldllycmp  23620  kgencmp2  23671  ptbasfi  23706  kqdisj  23857  kqcldsat  23858  trfbas2  23968  filss  23978  elfg  23996  flimclslem  24109  fcfneii  24162  tsmsfbas  24253  restutopopn  24363  ressxms  24650  restmetu  24695  qtopbaslem  24883  pi1addf  25174  pi1addval  25175  shftmbl  25665  voliunlem1  25677  voliunlem2  25678  uniioombllem2  25710  uniioombllem4  25713  uniioombllem6  25715  volsup2  25732  volcn  25733  volivth  25734  itg1climres  25841  limciun  26021  dvres3a  26041  ig1pval  26301  p1evtxdeqlem  29802  pthdlem2  30057  eupthp1  30507  omlsi  31696  pjoml  31728  chdmj3  31823  chdmj4  31824  ledi  31832  cmbr  31876  cmbr3  31900  pjoml3  31904  fh1  31910  fh2  31911  dmdbr  32591  dmdmd  32592  dmdbr5  32600  dmdsl3  32607  chirredlem2  32683  chirredlem3  32684  dmdbr6ati  32715  unidifsnne  32822  disji2f  32862  disjif2  32866  disjxpin  32873  disjunsn  32879  preiman0  32995  nn0diffz0  33079  cycpmco2f1  33384  tocyccntz  33404  oppr2idl  33712  isufd  33774  resssra  33921  dimkerim  33961  prsss  34250  carsgclctunlem1  34651  carsgclctunlem2  34653  carsgclctunlem3  34654  ballotlemfval  34824  signsplypnf  34881  ftc2re  34929  fsum2dsub  34938  bnj1326  35358  f1resfz0f1d  35503  pthhashvtx  35518  satfv1  35753  satefv  35804  mvrsval  35895  msrfval  35927  mthmpps  35972  elima4  36166  topbnd  36723  opnbnd  36724  cldbnd  36725  neibastop1  36758  neibastop2lem  36759  neibastop2  36760  neibastop3  36761  neifg  36770  dfttc4lem2  36928  bj-ismoored  37636  pibt2  37950  poimirlem3  38161  mblfinlem2  38196  ftc1anclem6  38236  heiborlem3  38351  cnvref4  38888  xrneq2  38937  disjressuc2  38949  elrefrels2  39136  refreleq  39139  elcnvrefrels2  39152  pmodN  40513  polvalN  40568  polatN  40594  trnsetN  40819  djavalN  41798  dihmeetbclemN  41967  dihmeetlem11N  41980  djhval  42061  lclkrlem2e  42174  lcfrlem23  42228  lcdlss2N  42283  elrfi  43316  elrfirn  43317  elrfirn2  43318  eldioph2lem1  43382  conrel2d  44281  ntrkbimka  44655  ntrk0kbimka  44656  isotone2  44666  ntrclskb  44686  ntrclsk3  44687  ntrclsk13  44688  clsneibex  44719  neicvgbex  44729  ismnushort  44902  relpfrlem  45553  inabs3  45667  disjiun2  45669  fresin2  45781  lptioo2  46238  lptioo1  46239  limsupvaluz  46313  cncfuni  46491  fourierdlem48  46759  fourierdlem49  46760  fourierdlem93  46804  qndenserrnbllem  46899  nnfoctbdjlem  47060  carageniuncllem1  47126  carageniuncllem2  47127  hoiqssbllem3  47229  smflimlem3  47378  smflim  47382  resinsnALT  49535  restclsseplem  49577