Theorem ineq2d 4173

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

Syntax hints:   → wi 4   = wceq 1570   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  rint0  4953  riin0  5048  disji2  5093  disjprg  5105  disjxun  5107  xpriindi  5822  riinint  5962  reseq2  5973  resindmOLD  6030  dfpo2  6297  csbpredg  6308  predep  6331  predprc  6339  predres  6340  onfr  6400  fimacnvinrn  7066  fimacnvinrn2  7067  isofrlem  7338  isoselem  7339  oev2  8504  domss2  9120  funsnfsupp  9348  kmlem11  10140  fpwwe2cbv  10610  fpwwe2lem3  10613  fpwwe2lem7  10617  fpwwe2lem11  10621  fpwwe2lem12  10622  fpwwe2  10623  fz1isolem  14494  limsupgle  15524  fsumm1  15798  incexclem  15886  bitsinv1  16495  bitsinvp1  16502  sadcadd  16511  sadadd2  16513  smumullem  16545  ressbas  17291  ressress  17302  restval  17474  ismred2  17650  cat1lem  18148  resscatc  18161  cnvps  18629  cntziinsn  19402  lsmdisj3r  19751  lsmdisj3b  19755  gsummptfzsplitl  19998  dmdprd  20065  subgdmdprd  20101  pgpfaclem1  20148  subrngpropd  20667  subrgpropd  20707  crng2idl  21420  obselocv  21878  basis1  23107  baspartn  23111  eltg  23114  tgdom  23135  indistopon  23158  ntrval  23193  clslp  23305  resttopon2  23325  restopnb  23332  paste  23451  nrmsep3  23512  imacmp  23554  cmpsub  23557  bwth  23567  llyi  23631  nllyi  23632  cldllycmp  23652  kgencmp2  23703  ptbasfi  23738  kqdisj  23889  kqcldsat  23890  trfbas2  24000  filss  24010  elfg  24028  flimclslem  24141  fcfneii  24194  tsmsfbas  24285  restutopopn  24395  ressxms  24682  restmetu  24727  qtopbaslem  24915  pi1addf  25206  pi1addval  25207  shftmbl  25697  voliunlem1  25709  voliunlem2  25710  uniioombllem2  25742  uniioombllem4  25745  uniioombllem6  25747  volsup2  25764  volcn  25765  volivth  25766  itg1climres  25873  limciun  26053  dvres3a  26073  ig1pval  26333  p1evtxdeqlem  29862  pthdlem2  30117  eupthp1  30567  omlsi  31756  pjoml  31788  chdmj3  31883  chdmj4  31884  ledi  31892  cmbr  31936  cmbr3  31960  pjoml3  31964  fh1  31970  fh2  31971  dmdbr  32651  dmdmd  32652  dmdbr5  32660  dmdsl3  32667  chirredlem2  32743  chirredlem3  32744  dmdbr6ati  32775  unidifsnne  32882  disji2f  32922  disjif2  32926  disjxpin  32933  disjunsn  32939  preiman0  33055  nn0diffz0  33139  cycpmco2f1  33444  tocyccntz  33464  oppr2idl  33768  isufd  33830  resssra  33977  dimkerim  34017  prsss  34306  carsgclctunlem1  34707  carsgclctunlem2  34709  carsgclctunlem3  34710  ballotlemfval  34880  signsplypnf  34937  ftc2re  34985  fsum2dsub  34994  bnj1326  35414  f1resfz0f1d  35605  pthhashvtx  35620  satfv1  35855  satefv  35906  mvrsval  35997  msrfval  36029  mthmpps  36074  elima4  36268  topbnd  36835  opnbnd  36836  cldbnd  36837  neibastop1  36870  neibastop2lem  36871  neibastop2  36872  neibastop3  36873  neifg  36882  dfttc4lem2  37040  bj-ismoored  37749  pibt2  38063  poimirlem3  38274  mblfinlem2  38309  ftc1anclem6  38349  heiborlem3  38464  cnvref4  38999  xrneq2  39048  disjressuc2  39060  elrefrels2  39247  refreleq  39250  elcnvrefrels2  39263  pmodN  40624  polvalN  40679  polatN  40705  trnsetN  40930  djavalN  41909  dihmeetbclemN  42078  dihmeetlem11N  42091  djhval  42172  lclkrlem2e  42285  lcfrlem23  42339  lcdlss2N  42394  elrfi  43425  elrfirn  43426  elrfirn2  43427  eldioph2lem1  43491  conrel2d  44390  ntrkbimka  44764  ntrk0kbimka  44765  isotone2  44775  ntrclskb  44795  ntrclsk3  44796  ntrclsk13  44797  clsneibex  44828  neicvgbex  44838  ismnushort  45011  relpfrlem  45662  inabs3  45776  disjiun2  45778  fresin2  45890  lptioo2  46347  lptioo1  46348  limsupvaluz  46422  cncfuni  46600  fourierdlem48  46868  fourierdlem49  46869  fourierdlem93  46913  qndenserrnbllem  47008  nnfoctbdjlem  47169  carageniuncllem1  47235  carageniuncllem2  47236  hoiqssbllem3  47338  smflimlem3  47487  smflim  47491  resinsnALT  49651  restclsseplem  49693