Theorem ineq2d 4167

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  rint0  4936  riin0  5028  disji2  5073  disjprg  5085  disjxun  5087  xpriindi  5775  riinint  5910  reseq2  5922  resindm  5978  dfpo2  6243  csbpredg  6254  predep  6277  predprc  6285  predres  6286  onfr  6345  fimacnvinrn  7004  fimacnvinrn2  7005  isofrlem  7274  isoselem  7275  oev2  8438  domss2  9049  funsnfsupp  9276  kmlem11  10052  fpwwe2cbv  10521  fpwwe2lem3  10524  fpwwe2lem7  10528  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  fz1isolem  14368  limsupgle  15384  fsumm1  15658  incexclem  15743  bitsinv1  16353  bitsinvp1  16360  sadcadd  16369  sadadd2  16371  smumullem  16403  ressbas  17147  ressress  17158  restval  17330  ismred2  17505  cat1lem  18003  resscatc  18016  cnvps  18484  cntziinsn  19249  lsmdisj3r  19598  lsmdisj3b  19602  gsummptfzsplitl  19845  dmdprd  19912  subgdmdprd  19948  pgpfaclem1  19995  subrngpropd  20483  subrgpropd  20523  crng2idl  21218  obselocv  21665  basis1  22865  baspartn  22869  eltg  22872  tgdom  22893  indistopon  22916  ntrval  22951  clslp  23063  resttopon2  23083  restopnb  23090  paste  23209  nrmsep3  23270  imacmp  23312  cmpsub  23315  bwth  23325  llyi  23389  nllyi  23390  cldllycmp  23410  kgencmp2  23461  ptbasfi  23496  kqdisj  23647  kqcldsat  23648  trfbas2  23758  filss  23768  elfg  23786  flimclslem  23899  fcfneii  23952  tsmsfbas  24043  restutopopn  24153  ressxms  24440  restmetu  24485  qtopbaslem  24673  pi1addf  24974  pi1addval  24975  shftmbl  25466  voliunlem1  25478  voliunlem2  25479  uniioombllem2  25511  uniioombllem4  25514  uniioombllem6  25516  volsup2  25533  volcn  25534  volivth  25535  itg1climres  25642  limciun  25822  dvres3a  25842  ig1pval  26108  p1evtxdeqlem  29491  pthdlem2  29746  eupthp1  30196  omlsi  31384  pjoml  31416  chdmj3  31511  chdmj4  31512  ledi  31520  cmbr  31564  cmbr3  31588  pjoml3  31592  fh1  31598  fh2  31599  dmdbr  32279  dmdmd  32280  dmdbr5  32288  dmdsl3  32295  chirredlem2  32371  chirredlem3  32372  dmdbr6ati  32403  unidifsnne  32516  disji2f  32557  disjif2  32561  disjxpin  32568  disjunsn  32574  preiman0  32691  cycpmco2f1  33093  tocyccntz  33113  oppr2idl  33451  isufd  33505  resssra  33599  dimkerim  33640  prsss  33929  carsgclctunlem1  34330  carsgclctunlem2  34332  carsgclctunlem3  34333  ballotlemfval  34503  signsplypnf  34563  ftc2re  34611  fsum2dsub  34620  bnj1326  35038  f1resfz0f1d  35158  pthhashvtx  35172  satfv1  35407  satefv  35458  mvrsval  35549  msrfval  35581  mthmpps  35626  elima4  35820  topbnd  36366  opnbnd  36367  cldbnd  36368  neibastop1  36401  neibastop2lem  36402  neibastop2  36403  neibastop3  36404  neifg  36413  bj-ismoored  37149  pibt2  37459  poimirlem3  37671  mblfinlem2  37706  ftc1anclem6  37746  heiborlem3  37861  cnvref4  38386  xrneq2  38420  disjressuc2  38428  elrefrels2  38563  refreleq  38566  elcnvrefrels2  38579  pmodN  39897  polvalN  39952  polatN  39978  trnsetN  40203  djavalN  41182  dihmeetbclemN  41351  dihmeetlem11N  41364  djhval  41445  lclkrlem2e  41558  lcfrlem23  41612  lcdlss2N  41667  elrfi  42735  elrfirn  42736  elrfirn2  42737  eldioph2lem1  42801  conrel2d  43705  ntrkbimka  44079  ntrk0kbimka  44080  isotone2  44090  ntrclskb  44110  ntrclsk3  44111  ntrclsk13  44112  clsneibex  44143  neicvgbex  44153  ismnushort  44342  relpfrlem  44994  inabs3  45101  disjiun2  45103  fresin2  45217  lptioo2  45679  lptioo1  45680  limsupvaluz  45754  cncfuni  45932  fourierdlem48  46200  fourierdlem49  46201  fourierdlem93  46245  qndenserrnbllem  46340  nnfoctbdjlem  46501  carageniuncllem1  46567  carageniuncllem2  46568  hoiqssbllem3  46670  smflimlem3  46819  smflim  46823  resinsnALT  48912  restclsseplem  48954