Theorem ineq2d 4160

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  rint0  4930  riin0  5024  disji2  5069  disjprg  5081  disjxun  5083  xpriindi  5791  riinint  5927  reseq2  5939  resindm  5995  dfpo2  6260  csbpredg  6271  predep  6294  predprc  6302  predres  6303  onfr  6362  fimacnvinrn  7023  fimacnvinrn2  7024  isofrlem  7295  isoselem  7296  oev2  8458  domss2  9074  funsnfsupp  9305  kmlem11  10083  fpwwe2cbv  10553  fpwwe2lem3  10556  fpwwe2lem7  10560  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  fz1isolem  14423  limsupgle  15439  fsumm1  15713  incexclem  15801  bitsinv1  16411  bitsinvp1  16418  sadcadd  16427  sadadd2  16429  smumullem  16461  ressbas  17206  ressress  17217  restval  17389  ismred2  17565  cat1lem  18063  resscatc  18076  cnvps  18544  cntziinsn  19312  lsmdisj3r  19661  lsmdisj3b  19665  gsummptfzsplitl  19908  dmdprd  19975  subgdmdprd  20011  pgpfaclem1  20058  subrngpropd  20545  subrgpropd  20585  crng2idl  21279  obselocv  21708  basis1  22915  baspartn  22919  eltg  22922  tgdom  22943  indistopon  22966  ntrval  23001  clslp  23113  resttopon2  23133  restopnb  23140  paste  23259  nrmsep3  23320  imacmp  23362  cmpsub  23365  bwth  23375  llyi  23439  nllyi  23440  cldllycmp  23460  kgencmp2  23511  ptbasfi  23546  kqdisj  23697  kqcldsat  23698  trfbas2  23808  filss  23818  elfg  23836  flimclslem  23949  fcfneii  24002  tsmsfbas  24093  restutopopn  24203  ressxms  24490  restmetu  24535  qtopbaslem  24723  pi1addf  25014  pi1addval  25015  shftmbl  25505  voliunlem1  25517  voliunlem2  25518  uniioombllem2  25550  uniioombllem4  25553  uniioombllem6  25555  volsup2  25572  volcn  25573  volivth  25574  itg1climres  25681  limciun  25861  dvres3a  25881  ig1pval  26141  p1evtxdeqlem  29581  pthdlem2  29836  eupthp1  30286  omlsi  31475  pjoml  31507  chdmj3  31602  chdmj4  31603  ledi  31611  cmbr  31655  cmbr3  31679  pjoml3  31683  fh1  31689  fh2  31690  dmdbr  32370  dmdmd  32371  dmdbr5  32379  dmdsl3  32386  chirredlem2  32462  chirredlem3  32463  dmdbr6ati  32494  unidifsnne  32606  disji2f  32647  disjif2  32651  disjxpin  32658  disjunsn  32664  preiman0  32783  nn0diffz0  32867  cycpmco2f1  33185  tocyccntz  33205  oppr2idl  33546  isufd  33600  resssra  33731  dimkerim  33771  prsss  34060  carsgclctunlem1  34461  carsgclctunlem2  34463  carsgclctunlem3  34464  ballotlemfval  34634  signsplypnf  34694  ftc2re  34742  fsum2dsub  34751  bnj1326  35168  f1resfz0f1d  35296  pthhashvtx  35310  satfv1  35545  satefv  35596  mvrsval  35687  msrfval  35719  mthmpps  35764  elima4  35958  topbnd  36506  opnbnd  36507  cldbnd  36508  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  neibastop3  36544  neifg  36553  dfttc4lem2  36711  bj-ismoored  37419  pibt2  37733  poimirlem3  37944  mblfinlem2  37979  ftc1anclem6  38019  heiborlem3  38134  cnvref4  38671  xrneq2  38720  disjressuc2  38732  elrefrels2  38919  refreleq  38922  elcnvrefrels2  38935  pmodN  40296  polvalN  40351  polatN  40377  trnsetN  40602  djavalN  41581  dihmeetbclemN  41750  dihmeetlem11N  41763  djhval  41844  lclkrlem2e  41957  lcfrlem23  42011  lcdlss2N  42066  elrfi  43126  elrfirn  43127  elrfirn2  43128  eldioph2lem1  43192  conrel2d  44091  ntrkbimka  44465  ntrk0kbimka  44466  isotone2  44476  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  clsneibex  44529  neicvgbex  44539  ismnushort  44728  relpfrlem  45380  inabs3  45487  disjiun2  45489  fresin2  45602  lptioo2  46061  lptioo1  46062  limsupvaluz  46136  cncfuni  46314  fourierdlem48  46582  fourierdlem49  46583  fourierdlem93  46627  qndenserrnbllem  46722  nnfoctbdjlem  46883  carageniuncllem1  46949  carageniuncllem2  46950  hoiqssbllem3  47052  smflimlem3  47201  smflim  47205  resinsnALT  49348  restclsseplem  49390