Theorem ineq2d 4174

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-in 3910

This theorem is referenced by:  rint0  4945  riin0  5039  disji2  5084  disjprg  5096  disjxun  5098  xpriindi  5793  riinint  5929  reseq2  5941  resindm  5997  dfpo2  6262  csbpredg  6273  predep  6296  predprc  6304  predres  6305  onfr  6364  fimacnvinrn  7025  fimacnvinrn2  7026  isofrlem  7296  isoselem  7297  oev2  8460  domss2  9076  funsnfsupp  9307  kmlem11  10083  fpwwe2cbv  10553  fpwwe2lem3  10556  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  fz1isolem  14396  limsupgle  15412  fsumm1  15686  incexclem  15771  bitsinv1  16381  bitsinvp1  16388  sadcadd  16397  sadadd2  16399  smumullem  16431  ressbas  17175  ressress  17186  restval  17358  ismred2  17534  cat1lem  18032  resscatc  18045  cnvps  18513  cntziinsn  19278  lsmdisj3r  19627  lsmdisj3b  19631  gsummptfzsplitl  19874  dmdprd  19941  subgdmdprd  19977  pgpfaclem1  20024  subrngpropd  20513  subrgpropd  20553  crng2idl  21248  obselocv  21695  basis1  22906  baspartn  22910  eltg  22913  tgdom  22934  indistopon  22957  ntrval  22992  clslp  23104  resttopon2  23124  restopnb  23131  paste  23250  nrmsep3  23311  imacmp  23353  cmpsub  23356  bwth  23366  llyi  23430  nllyi  23431  cldllycmp  23451  kgencmp2  23502  ptbasfi  23537  kqdisj  23688  kqcldsat  23689  trfbas2  23799  filss  23809  elfg  23827  flimclslem  23940  fcfneii  23993  tsmsfbas  24084  restutopopn  24194  ressxms  24481  restmetu  24526  qtopbaslem  24714  pi1addf  25015  pi1addval  25016  shftmbl  25507  voliunlem1  25519  voliunlem2  25520  uniioombllem2  25552  uniioombllem4  25555  uniioombllem6  25557  volsup2  25574  volcn  25575  volivth  25576  itg1climres  25683  limciun  25863  dvres3a  25883  ig1pval  26149  p1evtxdeqlem  29598  pthdlem2  29853  eupthp1  30303  omlsi  31492  pjoml  31524  chdmj3  31619  chdmj4  31620  ledi  31628  cmbr  31672  cmbr3  31696  pjoml3  31700  fh1  31706  fh2  31707  dmdbr  32387  dmdmd  32388  dmdbr5  32396  dmdsl3  32403  chirredlem2  32479  chirredlem3  32480  dmdbr6ati  32511  unidifsnne  32623  disji2f  32664  disjif2  32668  disjxpin  32675  disjunsn  32681  preiman0  32800  nn0diffz0  32885  cycpmco2f1  33218  tocyccntz  33238  oppr2idl  33579  isufd  33633  resssra  33764  dimkerim  33805  prsss  34094  carsgclctunlem1  34495  carsgclctunlem2  34497  carsgclctunlem3  34498  ballotlemfval  34668  signsplypnf  34728  ftc2re  34776  fsum2dsub  34785  bnj1326  35202  f1resfz0f1d  35330  pthhashvtx  35344  satfv1  35579  satefv  35630  mvrsval  35721  msrfval  35753  mthmpps  35798  elima4  35992  topbnd  36540  opnbnd  36541  cldbnd  36542  neibastop1  36575  neibastop2lem  36576  neibastop2  36577  neibastop3  36578  neifg  36587  bj-ismoored  37360  pibt2  37672  poimirlem3  37874  mblfinlem2  37909  ftc1anclem6  37949  heiborlem3  38064  cnvref4  38601  xrneq2  38650  disjressuc2  38662  elrefrels2  38849  refreleq  38852  elcnvrefrels2  38865  pmodN  40226  polvalN  40281  polatN  40307  trnsetN  40532  djavalN  41511  dihmeetbclemN  41680  dihmeetlem11N  41693  djhval  41774  lclkrlem2e  41887  lcfrlem23  41941  lcdlss2N  41996  elrfi  43051  elrfirn  43052  elrfirn2  43053  eldioph2lem1  43117  conrel2d  44020  ntrkbimka  44394  ntrk0kbimka  44395  isotone2  44405  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  clsneibex  44458  neicvgbex  44468  ismnushort  44657  relpfrlem  45309  inabs3  45416  disjiun2  45418  fresin2  45531  lptioo2  45991  lptioo1  45992  limsupvaluz  46066  cncfuni  46244  fourierdlem48  46512  fourierdlem49  46513  fourierdlem93  46557  qndenserrnbllem  46652  nnfoctbdjlem  46813  carageniuncllem1  46879  carageniuncllem2  46880  hoiqssbllem3  46982  smflimlem3  47131  smflim  47135  resinsnALT  49232  restclsseplem  49274