Theorem ineq1d 4172

Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)

Hypothesis

Ref	Expression
ineq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ineq1d	⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

Proof of Theorem ineq1d

Step	Hyp	Ref	Expression
1		ineq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ineq1 4166	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

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

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-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-in 3912

This theorem is referenced by:  iinrab2  5022  disji2  5079  disjprg  5091  disjxun  5093  riinint  5917  fnresdisj  6606  fnimadisj  6618  fninfp  7114  ecinxp  8726  fiint  9235  fiintOLD  9236  fival  9321  marypha1lem  9342  kmlem12  10075  fin23lem12  10244  fin23lem30  10255  fin23lem33  10258  ttukeylem1  10422  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwe2  10556  fzval2  13432  fvinim0ffz  13708  limsupval  15400  limsupgval  15402  ello1  15441  elo1  15452  fsum1p  15679  incexclem  15762  fprod1p  15894  smuval2  16412  smueqlem  16420  smumul  16423  setsdm  17100  isacs2  17578  acsfiel  17579  isacs1i  17582  cat1lem  18022  catcval  18026  resscatc  18035  acsficl  18472  lsmdisj3  19581  lsmdisj3a  19587  dprdres  19928  dprdz  19930  dpjdisj  19953  lspdisj2  21053  indistopon  22905  restopnb  23079  ordtrest2  23108  isnrm  23239  cmpcov  23293  cmpsublem  23303  cmpsub  23304  tgcmp  23305  uncmp  23307  hauscmplem  23310  nconnsubb  23327  isnlly  23373  dissnlocfin  23433  kgeni  23441  kgencn3  23462  ptcld  23517  ptcnplem  23525  alexsublem  23948  alexsubb  23950  alexsubALTlem2  23952  alexsubALTlem4  23954  alexsubALT  23955  tmdgsum2  24000  tsmsval2  24034  ustexsym  24120  metrest  24429  qtopbaslem  24663  cnheibor  24871  bndth  24874  lebnumii  24882  iscph  25087  csscld  25166  clsocv  25167  cphsscph  25168  ovolicc2  25440  voliunlem3  25470  ioombl  25483  uniioombllem2  25501  uniioombllem4  25504  uniioombllem6  25506  mbflimsup  25584  taylfval  26283  chtval  27037  ppival  27054  ppival2  27055  ppival2g  27056  chtfl  27076  ppiprm  27078  chtprm  27080  chtnprm  27081  chtdif  27085  ppidif  27090  prmorcht  27105  nosupbnd2lem1  27644  dfpth2  29693  chdmj2  31493  cmcmlem  31554  pjoml2  31574  fh2  31582  mdbr  32257  mdi  32258  mdbr3  32260  mdbr4  32261  dmdmd  32263  dmdbr3  32268  dmdbr4  32269  dmdi4  32270  dmdbr5  32271  mddmd2  32272  mdsl1i  32284  cvmdi  32287  mdslmd1lem1  32288  mdslmd1lem2  32289  mdslmd1lem3  32290  mdslmd1lem4  32291  mdslmd1i  32292  mdslmd3i  32295  csmdsymi  32297  mdexchi  32298  atomli  32345  atabsi  32364  sumdmdlem2  32382  dmdbr5ati  32385  difuncomp  32516  disji2f  32540  disjif2  32544  disjxpin  32551  disjunsn  32557  fnresin  32587  cycpmco2f1  33085  cycpmconjslem2  33116  locfinreflem  33826  iscref  33830  ordtrest2NEW  33909  ordtconnlem1  33910  carsgclctunlem1  34304  totprobd  34413  probmeasb  34417  ballotlemfval  34477  ballotlemfp1  34479  ballotlemgun  34512  chtvalz  34616  bnj1385  34818  bnj1326  35012  vonf1owev  35100  iccllysconn  35242  satfv1  35355  mvrsval  35497  mrsubvrs  35514  mpstval  35527  msubvrs  35552  neibastop2lem  36353  neibastop2  36354  neibastop3  36355  limsucncmpi  36438  bj-ismoore  37098  fvineqsnf1  37403  pibt2  37410  ptrest  37618  mblfinlem2  37657  sstotbnd2  37773  cntotbnd  37795  heibor  37820  xrneq1  38368  disjressuc2  38379  l1cvat  39053  pmodlem2  39846  pmod2iN  39848  hlmod1i  39855  osumcllem3N  39957  osumcllem9N  39963  pexmidlem6N  39974  pl42lem1N  39978  istrnN  40156  djavalN  41134  dihmeetlem9N  41314  dihmeetlem11N  41316  dihmeetlem12N  41317  dihoml4  41376  djhval  41397  dochexmidlem6  41464  lclkrlem2b  41507  lcfrlem20  41561  lcfrlem23  41564  elrfi  42687  isnacs  42697  mrefg2  42700  mapfzcons2  42712  coeq0i  42746  eldioph2lem2  42754  aomclem8  43054  kelac1  43056  islmodfg  43062  lnr2i  43109  fgraphopab  43196  ntrkbimka  44031  ntrk0kbimka  44032  isotone2  44042  ntrclskb  44062  ntrclsk3  44063  ntrclsk13  44064  neicvgbex  44105  disjrnmpt2  45186  disjinfi  45190  uzinico2  45562  uzinico3  45563  fsumiunss  45576  lptre2pt  45641  limsupresre  45697  limsuplesup  45700  limsupresico  45701  limsupvaluz  45709  limsuplt2  45754  liminfval  45760  limsupge  45762  liminfgval  45763  liminfval2  45769  liminfresico  45772  liminflelimsuplem  45776  liminflelimsup  45777  stoweidlem50  46051  stoweidlem57  46058  subsaliuncllem  46358  sge0val  46367  sge0iunmptlemre  46416  nnfoctbdjlem  46456  iundjiun  46461  vonvolmbllem  46661  smfpimcclem  46808  smfsuplem1  46812  f1cof1blem  47078  3f1oss1  47079  grimuhgr  47891  elbigo  48556  restclsseplem  48919  sepnsepo  48928  aacllem  49806