Theorem ineq2d 4179

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  rint0  4948  riin0  5041  disji2  5086  disjprg  5098  disjxun  5100  xpriindi  5790  riinint  5924  reseq2  5934  resindm  5990  dfpo2  6257  csbpredg  6268  predep  6291  predprc  6299  predres  6300  onfr  6359  fimacnvinrn  7025  fimacnvinrn2  7026  isofrlem  7297  isoselem  7298  oev2  8464  domss2  9077  funsnfsupp  9319  kmlem11  10090  fpwwe2cbv  10559  fpwwe2lem3  10562  fpwwe2lem7  10566  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  fz1isolem  14402  limsupgle  15419  fsumm1  15693  incexclem  15778  bitsinv1  16388  bitsinvp1  16395  sadcadd  16404  sadadd2  16406  smumullem  16438  ressbas  17182  ressress  17193  restval  17365  ismred2  17540  cat1lem  18034  resscatc  18047  cnvps  18513  cntziinsn  19245  lsmdisj3r  19592  lsmdisj3b  19596  gsummptfzsplitl  19839  dmdprd  19906  subgdmdprd  19942  pgpfaclem1  19989  subrngpropd  20453  subrgpropd  20493  crng2idl  21167  obselocv  21613  basis1  22813  baspartn  22817  eltg  22820  tgdom  22841  indistopon  22864  ntrval  22899  clslp  23011  resttopon2  23031  restopnb  23038  paste  23157  nrmsep3  23218  imacmp  23260  cmpsub  23263  bwth  23273  llyi  23337  nllyi  23338  cldllycmp  23358  kgencmp2  23409  ptbasfi  23444  kqdisj  23595  kqcldsat  23596  trfbas2  23706  filss  23716  elfg  23734  flimclslem  23847  fcfneii  23900  tsmsfbas  23991  restutopopn  24102  ressxms  24389  restmetu  24434  qtopbaslem  24622  pi1addf  24923  pi1addval  24924  shftmbl  25415  voliunlem1  25427  voliunlem2  25428  uniioombllem2  25460  uniioombllem4  25463  uniioombllem6  25465  volsup2  25482  volcn  25483  volivth  25484  itg1climres  25591  limciun  25771  dvres3a  25791  ig1pval  26057  p1evtxdeqlem  29416  pthdlem2  29671  eupthp1  30118  omlsi  31306  pjoml  31338  chdmj3  31433  chdmj4  31434  ledi  31442  cmbr  31486  cmbr3  31510  pjoml3  31514  fh1  31520  fh2  31521  dmdbr  32201  dmdmd  32202  dmdbr5  32210  dmdsl3  32217  chirredlem2  32293  chirredlem3  32294  dmdbr6ati  32325  unidifsnne  32438  disji2f  32479  disjif2  32483  disjxpin  32490  disjunsn  32496  preiman0  32606  cycpmco2f1  33054  tocyccntz  33074  oppr2idl  33430  isufd  33484  resssra  33556  dimkerim  33596  prsss  33879  carsgclctunlem1  34281  carsgclctunlem2  34283  carsgclctunlem3  34284  ballotlemfval  34454  signsplypnf  34514  ftc2re  34562  fsum2dsub  34571  bnj1326  34989  f1resfz0f1d  35074  pthhashvtx  35088  satfv1  35323  satefv  35374  mvrsval  35465  msrfval  35497  mthmpps  35542  elima4  35736  topbnd  36285  opnbnd  36286  cldbnd  36287  neibastop1  36320  neibastop2lem  36321  neibastop2  36322  neibastop3  36323  neifg  36332  bj-ismoored  37068  pibt2  37378  poimirlem3  37590  mblfinlem2  37625  ftc1anclem6  37665  heiborlem3  37780  cnvref4  38305  xrneq2  38339  disjressuc2  38347  elrefrels2  38482  refreleq  38485  elcnvrefrels2  38498  pmodN  39817  polvalN  39872  polatN  39898  trnsetN  40123  djavalN  41102  dihmeetbclemN  41271  dihmeetlem11N  41284  djhval  41365  lclkrlem2e  41478  lcfrlem23  41532  lcdlss2N  41587  elrfi  42655  elrfirn  42656  elrfirn2  42657  eldioph2lem1  42721  conrel2d  43626  ntrkbimka  44000  ntrk0kbimka  44001  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  clsneibex  44064  neicvgbex  44074  ismnushort  44263  relpfrlem  44916  inabs3  45023  disjiun2  45025  fresin2  45139  lptioo2  45602  lptioo1  45603  limsupvaluz  45679  cncfuni  45857  fourierdlem48  46125  fourierdlem49  46126  fourierdlem93  46170  qndenserrnbllem  46265  nnfoctbdjlem  46426  carageniuncllem1  46492  carageniuncllem2  46493  hoiqssbllem3  46595  smflimlem3  46744  smflim  46748  resinsnALT  48834  restclsseplem  48876