Theorem ineq2d 4161

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

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

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 3391  df-in 3897

This theorem is referenced by:  rint0  4931  riin0  5025  disji2  5070  disjprg  5082  disjxun  5084  xpriindi  5786  riinint  5922  reseq2  5934  resindm  5990  dfpo2  6255  csbpredg  6266  predep  6289  predprc  6297  predres  6298  onfr  6357  fimacnvinrn  7018  fimacnvinrn2  7019  isofrlem  7289  isoselem  7290  oev2  8452  domss2  9068  funsnfsupp  9299  kmlem11  10077  fpwwe2cbv  10547  fpwwe2lem3  10550  fpwwe2lem7  10554  fpwwe2lem11  10558  fpwwe2lem12  10559  fpwwe2  10560  fz1isolem  14417  limsupgle  15433  fsumm1  15707  incexclem  15795  bitsinv1  16405  bitsinvp1  16412  sadcadd  16421  sadadd2  16423  smumullem  16455  ressbas  17200  ressress  17211  restval  17383  ismred2  17559  cat1lem  18057  resscatc  18070  cnvps  18538  cntziinsn  19306  lsmdisj3r  19655  lsmdisj3b  19659  gsummptfzsplitl  19902  dmdprd  19969  subgdmdprd  20005  pgpfaclem1  20052  subrngpropd  20539  subrgpropd  20579  crng2idl  21274  obselocv  21721  basis1  22928  baspartn  22932  eltg  22935  tgdom  22956  indistopon  22979  ntrval  23014  clslp  23126  resttopon2  23146  restopnb  23153  paste  23272  nrmsep3  23333  imacmp  23375  cmpsub  23378  bwth  23388  llyi  23452  nllyi  23453  cldllycmp  23473  kgencmp2  23524  ptbasfi  23559  kqdisj  23710  kqcldsat  23711  trfbas2  23821  filss  23831  elfg  23849  flimclslem  23962  fcfneii  24015  tsmsfbas  24106  restutopopn  24216  ressxms  24503  restmetu  24548  qtopbaslem  24736  pi1addf  25027  pi1addval  25028  shftmbl  25518  voliunlem1  25530  voliunlem2  25531  uniioombllem2  25563  uniioombllem4  25566  uniioombllem6  25568  volsup2  25585  volcn  25586  volivth  25587  itg1climres  25694  limciun  25874  dvres3a  25894  ig1pval  26154  p1evtxdeqlem  29599  pthdlem2  29854  eupthp1  30304  omlsi  31493  pjoml  31525  chdmj3  31620  chdmj4  31621  ledi  31629  cmbr  31673  cmbr3  31697  pjoml3  31701  fh1  31707  fh2  31708  dmdbr  32388  dmdmd  32389  dmdbr5  32397  dmdsl3  32404  chirredlem2  32480  chirredlem3  32481  dmdbr6ati  32512  unidifsnne  32624  disji2f  32665  disjif2  32669  disjxpin  32676  disjunsn  32682  preiman0  32801  nn0diffz0  32885  cycpmco2f1  33203  tocyccntz  33223  oppr2idl  33564  isufd  33618  resssra  33749  dimkerim  33790  prsss  34079  carsgclctunlem1  34480  carsgclctunlem2  34482  carsgclctunlem3  34483  ballotlemfval  34653  signsplypnf  34713  ftc2re  34761  fsum2dsub  34770  bnj1326  35187  f1resfz0f1d  35315  pthhashvtx  35329  satfv1  35564  satefv  35615  mvrsval  35706  msrfval  35738  mthmpps  35783  elima4  35977  topbnd  36525  opnbnd  36526  cldbnd  36527  neibastop1  36560  neibastop2lem  36561  neibastop2  36562  neibastop3  36563  neifg  36572  dfttc4lem2  36730  bj-ismoored  37438  pibt2  37750  poimirlem3  37961  mblfinlem2  37996  ftc1anclem6  38036  heiborlem3  38151  cnvref4  38688  xrneq2  38737  disjressuc2  38749  elrefrels2  38936  refreleq  38939  elcnvrefrels2  38952  pmodN  40313  polvalN  40368  polatN  40394  trnsetN  40619  djavalN  41598  dihmeetbclemN  41767  dihmeetlem11N  41780  djhval  41861  lclkrlem2e  41974  lcfrlem23  42028  lcdlss2N  42083  elrfi  43143  elrfirn  43144  elrfirn2  43145  eldioph2lem1  43209  conrel2d  44112  ntrkbimka  44486  ntrk0kbimka  44487  isotone2  44497  ntrclskb  44517  ntrclsk3  44518  ntrclsk13  44519  clsneibex  44550  neicvgbex  44560  ismnushort  44749  relpfrlem  45401  inabs3  45508  disjiun2  45510  fresin2  45623  lptioo2  46082  lptioo1  46083  limsupvaluz  46157  cncfuni  46335  fourierdlem48  46603  fourierdlem49  46604  fourierdlem93  46648  qndenserrnbllem  46743  nnfoctbdjlem  46904  carageniuncllem1  46970  carageniuncllem2  46971  hoiqssbllem3  47073  smflimlem3  47222  smflim  47226  resinsnALT  49363  restclsseplem  49405