Theorem ineq1d 4160

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 4154	. 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-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:  iinrab2  5013  disji2  5070  disjprg  5082  disjxun  5084  riinint  5919  fnresdisj  6610  fnimadisj  6622  fninfp  7120  ecinxp  8730  fiint  9228  fival  9316  marypha1lem  9337  kmlem12  10073  fin23lem12  10242  fin23lem30  10253  fin23lem33  10256  ttukeylem1  10420  fpwwe2cbv  10542  fpwwe2lem2  10544  fpwwe2  10555  fzval2  13453  fvinim0ffz  13733  limsupval  15425  limsupgval  15427  ello1  15466  elo1  15477  fsum1p  15704  incexclem  15790  fprod1p  15922  smuval2  16440  smueqlem  16448  smumul  16451  setsdm  17129  isacs2  17608  acsfiel  17609  isacs1i  17612  cat1lem  18052  catcval  18056  resscatc  18065  acsficl  18502  lsmdisj3  19647  lsmdisj3a  19653  dprdres  19994  dprdz  19996  dpjdisj  20019  lspdisj2  21115  indistopon  22975  restopnb  23149  ordtrest2  23178  isnrm  23309  cmpcov  23363  cmpsublem  23373  cmpsub  23374  tgcmp  23375  uncmp  23377  hauscmplem  23380  nconnsubb  23397  isnlly  23443  dissnlocfin  23503  kgeni  23511  kgencn3  23532  ptcld  23587  ptcnplem  23595  alexsublem  24018  alexsubb  24020  alexsubALTlem2  24022  alexsubALTlem4  24024  alexsubALT  24025  tmdgsum2  24070  tsmsval2  24104  ustexsym  24190  metrest  24498  qtopbaslem  24732  cnheibor  24931  bndth  24934  lebnumii  24942  iscph  25146  csscld  25225  clsocv  25226  cphsscph  25227  ovolicc2  25498  voliunlem3  25528  ioombl  25541  uniioombllem2  25559  uniioombllem4  25562  uniioombllem6  25564  mbflimsup  25642  taylfval  26337  chtval  27091  ppival  27108  ppival2  27109  ppival2g  27110  chtfl  27130  ppiprm  27132  chtprm  27134  chtnprm  27135  chtdif  27139  ppidif  27144  prmorcht  27159  nosupbnd2lem1  27698  dfpth2  29817  chdmj2  31621  cmcmlem  31682  pjoml2  31702  fh2  31710  mdbr  32385  mdi  32386  mdbr3  32388  mdbr4  32389  dmdmd  32391  dmdbr3  32396  dmdbr4  32397  dmdi4  32398  dmdbr5  32399  mddmd2  32400  mdsl1i  32412  cvmdi  32415  mdslmd1lem1  32416  mdslmd1lem2  32417  mdslmd1lem3  32418  mdslmd1lem4  32419  mdslmd1i  32420  mdslmd3i  32423  csmdsymi  32425  mdexchi  32426  atomli  32473  atabsi  32492  sumdmdlem2  32510  dmdbr5ati  32513  difuncomp  32643  disji2f  32667  disjif2  32671  disjxpin  32678  disjunsn  32684  fnresin  32717  cycpmco2f1  33205  cycpmconjslem2  33236  locfinreflem  34005  iscref  34009  ordtrest2NEW  34088  ordtconnlem1  34089  carsgclctunlem1  34482  totprobd  34591  probmeasb  34595  ballotlemfval  34655  ballotlemfp1  34657  ballotlemgun  34690  chtvalz  34794  bnj1385  34995  bnj1326  35189  vonf1owev  35311  iccllysconn  35453  satfv1  35566  mvrsval  35708  mrsubvrs  35725  mpstval  35738  msubvrs  35763  neibastop2lem  36563  neibastop2  36564  neibastop3  36565  limsucncmpi  36648  dfttc4  36733  bj-ismoore  37430  fvineqsnf1  37737  pibt2  37744  ptrest  37951  mblfinlem2  37990  sstotbnd2  38106  cntotbnd  38128  heibor  38153  xrneq1  38728  disjressuc2  38743  ecqmap  38781  l1cvat  39512  pmodlem2  40304  pmod2iN  40306  hlmod1i  40313  osumcllem3N  40415  osumcllem9N  40421  pexmidlem6N  40432  pl42lem1N  40436  istrnN  40614  djavalN  41592  dihmeetlem9N  41772  dihmeetlem11N  41774  dihmeetlem12N  41775  dihoml4  41834  djhval  41855  dochexmidlem6  41922  lclkrlem2b  41965  lcfrlem20  42019  lcfrlem23  42022  elrfi  43137  isnacs  43147  mrefg2  43150  mapfzcons2  43162  coeq0i  43196  eldioph2lem2  43204  aomclem8  43504  kelac1  43506  islmodfg  43512  lnr2i  43559  fgraphopab  43646  ntrkbimka  44480  ntrk0kbimka  44481  isotone2  44491  ntrclskb  44511  ntrclsk3  44512  ntrclsk13  44513  neicvgbex  44554  disjrnmpt2  45633  disjinfi  45637  uzinico2  46006  uzinico3  46007  fsumiunss  46020  lptre2pt  46083  limsupresre  46139  limsuplesup  46142  limsupresico  46143  limsupvaluz  46151  limsuplt2  46196  liminfval  46202  limsupge  46204  liminfgval  46205  liminfval2  46211  liminfresico  46214  liminflelimsuplem  46218  liminflelimsup  46219  stoweidlem50  46493  stoweidlem57  46500  subsaliuncllem  46800  sge0val  46809  sge0iunmptlemre  46858  nnfoctbdjlem  46898  iundjiun  46903  vonvolmbllem  47103  smfpimcclem  47250  smfsuplem1  47254  f1cof1blem  47519  3f1oss1  47520  grimuhgr  48360  elbigo  49024  restclsseplem  49387  sepnsepo  49396  aacllem  50273