Theorem ineq1d 4142

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-in 3890

This theorem is referenced by:  iinrab2  4995  disji2  5052  disjprgw  5065  disjprg  5066  disjxun  5068  riinint  5866  fnresdisj  6536  fnimadisj  6549  fninfp  7028  ecinxp  8539  fiint  9021  fival  9101  marypha1lem  9122  kmlem12  9848  fin23lem12  10018  fin23lem30  10029  fin23lem33  10032  ttukeylem1  10196  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwe2  10330  fzval2  13171  fvinim0ffz  13434  limsupval  15111  limsupgval  15113  ello1  15152  elo1  15163  fsum1p  15393  incexclem  15476  fprod1p  15606  smuval2  16117  smueqlem  16125  smumul  16128  setsdm  16799  isacs2  17279  acsfiel  17280  isacs1i  17283  cat1lem  17727  catcval  17731  resscatc  17740  acsficl  18180  lsmdisj3  19204  lsmdisj3a  19210  dprdres  19546  dprdz  19548  dpjdisj  19571  lspdisj2  20304  indistopon  22059  restopnb  22234  ordtrest2  22263  isnrm  22394  cmpcov  22448  cmpsublem  22458  cmpsub  22459  tgcmp  22460  uncmp  22462  hauscmplem  22465  nconnsubb  22482  isnlly  22528  dissnlocfin  22588  kgeni  22596  kgencn3  22617  ptcld  22672  ptcnplem  22680  alexsublem  23103  alexsubb  23105  alexsubALTlem2  23107  alexsubALTlem4  23109  alexsubALT  23110  tmdgsum2  23155  tsmsval2  23189  ustexsym  23275  metrest  23586  qtopbaslem  23828  cnheibor  24024  bndth  24027  lebnumii  24035  iscph  24239  csscld  24318  clsocv  24319  cphsscph  24320  ovolicc2  24591  voliunlem3  24621  ioombl  24634  uniioombllem2  24652  uniioombllem4  24655  uniioombllem6  24657  mbflimsup  24735  taylfval  25423  chtval  26164  ppival  26181  ppival2  26182  ppival2g  26183  chtfl  26203  ppiprm  26205  chtprm  26207  chtnprm  26208  chtdif  26212  ppidif  26217  prmorcht  26232  chdmj2  29793  cmcmlem  29854  pjoml2  29874  fh2  29882  mdbr  30557  mdi  30558  mdbr3  30560  mdbr4  30561  dmdmd  30563  dmdbr3  30568  dmdbr4  30569  dmdi4  30570  dmdbr5  30571  mddmd2  30572  mdsl1i  30584  cvmdi  30587  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd1lem3  30590  mdslmd1lem4  30591  mdslmd1i  30592  mdslmd3i  30595  csmdsymi  30597  mdexchi  30598  atomli  30645  atabsi  30664  sumdmdlem2  30682  dmdbr5ati  30685  difuncomp  30794  disji2f  30817  disjif2  30821  disjxpin  30828  disjunsn  30834  fnresin  30862  cycpmco2f1  31293  cycpmconjslem2  31324  locfinreflem  31692  iscref  31696  ordtrest2NEW  31775  ordtconnlem1  31776  carsgclctunlem1  32184  totprobd  32293  probmeasb  32297  ballotlemfval  32356  ballotlemfp1  32358  ballotlemgun  32391  chtvalz  32509  bnj1385  32712  bnj1326  32906  iccllysconn  33112  satfv1  33225  mvrsval  33367  mrsubvrs  33384  mpstval  33397  msubvrs  33422  nosupbnd2lem1  33845  neibastop2lem  34476  neibastop2  34477  neibastop3  34478  limsucncmpi  34561  bj-ismoore  35203  fvineqsnf1  35508  pibt2  35515  ptrest  35703  mblfinlem2  35742  sstotbnd2  35859  cntotbnd  35881  heibor  35906  xrneq1  36434  l1cvat  36996  pmodlem2  37788  pmod2iN  37790  hlmod1i  37797  osumcllem3N  37899  osumcllem9N  37905  pexmidlem6N  37916  pl42lem1N  37920  istrnN  38098  djavalN  39076  dihmeetlem9N  39256  dihmeetlem11N  39258  dihmeetlem12N  39259  dihoml4  39318  djhval  39339  dochexmidlem6  39406  lclkrlem2b  39449  lcfrlem20  39503  lcfrlem23  39506  metakunt20  40072  elrfi  40432  isnacs  40442  mrefg2  40445  mapfzcons2  40457  coeq0i  40491  eldioph2lem2  40499  aomclem8  40802  kelac1  40804  islmodfg  40810  lnr2i  40857  fgraphopab  40951  ntrkbimka  41537  ntrk0kbimka  41538  isotone2  41548  ntrclskb  41568  ntrclsk3  41569  ntrclsk13  41570  neicvgbex  41611  disjrnmpt2  42615  disjinfi  42620  uzinico2  42990  uzinico3  42991  fsumiunss  43006  lptre2pt  43071  limsupresre  43127  limsuplesup  43130  limsupresico  43131  limsupvaluz  43139  limsuplt2  43184  liminfval  43190  limsupge  43192  liminfgval  43193  liminfval2  43199  liminfresico  43202  liminflelimsuplem  43206  liminflelimsup  43207  stoweidlem50  43481  stoweidlem57  43488  subsaliuncllem  43786  sge0val  43794  sge0iunmptlemre  43843  nnfoctbdjlem  43883  iundjiun  43888  vonvolmbllem  44088  smfpimcclem  44227  smfsuplem1  44231  f1cof1blem  44455  elbigo  45785  restclsseplem  46096  sepnsepo  46105  aacllem  46391