Theorem ineq1d 4146

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-in 3895

This theorem is referenced by:  iinrab2  5000  disji2  5057  disjprgw  5070  disjprg  5071  disjxun  5073  riinint  5880  fnresdisj  6561  fnimadisj  6574  fninfp  7055  ecinxp  8590  fiint  9100  fival  9180  marypha1lem  9201  kmlem12  9926  fin23lem12  10096  fin23lem30  10107  fin23lem33  10110  ttukeylem1  10274  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwe2  10408  fzval2  13251  fvinim0ffz  13515  limsupval  15192  limsupgval  15194  ello1  15233  elo1  15244  fsum1p  15474  incexclem  15557  fprod1p  15687  smuval2  16198  smueqlem  16206  smumul  16209  setsdm  16880  isacs2  17371  acsfiel  17372  isacs1i  17375  cat1lem  17820  catcval  17824  resscatc  17833  acsficl  18274  lsmdisj3  19298  lsmdisj3a  19304  dprdres  19640  dprdz  19642  dpjdisj  19665  lspdisj2  20398  indistopon  22160  restopnb  22335  ordtrest2  22364  isnrm  22495  cmpcov  22549  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  hauscmplem  22566  nconnsubb  22583  isnlly  22629  dissnlocfin  22689  kgeni  22697  kgencn3  22718  ptcld  22773  ptcnplem  22781  alexsublem  23204  alexsubb  23206  alexsubALTlem2  23208  alexsubALTlem4  23210  alexsubALT  23211  tmdgsum2  23256  tsmsval2  23290  ustexsym  23376  metrest  23689  qtopbaslem  23931  cnheibor  24127  bndth  24130  lebnumii  24138  iscph  24343  csscld  24422  clsocv  24423  cphsscph  24424  ovolicc2  24695  voliunlem3  24725  ioombl  24738  uniioombllem2  24756  uniioombllem4  24759  uniioombllem6  24761  mbflimsup  24839  taylfval  25527  chtval  26268  ppival  26285  ppival2  26286  ppival2g  26287  chtfl  26307  ppiprm  26309  chtprm  26311  chtnprm  26312  chtdif  26316  ppidif  26321  prmorcht  26336  chdmj2  29901  cmcmlem  29962  pjoml2  29982  fh2  29990  mdbr  30665  mdi  30666  mdbr3  30668  mdbr4  30669  dmdmd  30671  dmdbr3  30676  dmdbr4  30677  dmdi4  30678  dmdbr5  30679  mddmd2  30680  mdsl1i  30692  cvmdi  30695  mdslmd1lem1  30696  mdslmd1lem2  30697  mdslmd1lem3  30698  mdslmd1lem4  30699  mdslmd1i  30700  mdslmd3i  30703  csmdsymi  30705  mdexchi  30706  atomli  30753  atabsi  30772  sumdmdlem2  30790  dmdbr5ati  30793  difuncomp  30902  disji2f  30925  disjif2  30929  disjxpin  30936  disjunsn  30942  fnresin  30970  cycpmco2f1  31400  cycpmconjslem2  31431  locfinreflem  31799  iscref  31803  ordtrest2NEW  31882  ordtconnlem1  31883  carsgclctunlem1  32293  totprobd  32402  probmeasb  32406  ballotlemfval  32465  ballotlemfp1  32467  ballotlemgun  32500  chtvalz  32618  bnj1385  32821  bnj1326  33015  iccllysconn  33221  satfv1  33334  mvrsval  33476  mrsubvrs  33493  mpstval  33506  msubvrs  33531  nosupbnd2lem1  33927  neibastop2lem  34558  neibastop2  34559  neibastop3  34560  limsucncmpi  34643  bj-ismoore  35285  fvineqsnf1  35590  pibt2  35597  ptrest  35785  mblfinlem2  35824  sstotbnd2  35941  cntotbnd  35963  heibor  35988  xrneq1  36514  l1cvat  37076  pmodlem2  37868  pmod2iN  37870  hlmod1i  37877  osumcllem3N  37979  osumcllem9N  37985  pexmidlem6N  37996  pl42lem1N  38000  istrnN  38178  djavalN  39156  dihmeetlem9N  39336  dihmeetlem11N  39338  dihmeetlem12N  39339  dihoml4  39398  djhval  39419  dochexmidlem6  39486  lclkrlem2b  39529  lcfrlem20  39583  lcfrlem23  39586  metakunt20  40151  elrfi  40523  isnacs  40533  mrefg2  40536  mapfzcons2  40548  coeq0i  40582  eldioph2lem2  40590  aomclem8  40893  kelac1  40895  islmodfg  40901  lnr2i  40948  fgraphopab  41042  ntrkbimka  41655  ntrk0kbimka  41656  isotone2  41666  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  neicvgbex  41729  disjrnmpt2  42733  disjinfi  42738  uzinico2  43107  uzinico3  43108  fsumiunss  43123  lptre2pt  43188  limsupresre  43244  limsuplesup  43247  limsupresico  43248  limsupvaluz  43256  limsuplt2  43301  liminfval  43307  limsupge  43309  liminfgval  43310  liminfval2  43316  liminfresico  43319  liminflelimsuplem  43323  liminflelimsup  43324  stoweidlem50  43598  stoweidlem57  43605  subsaliuncllem  43903  sge0val  43911  sge0iunmptlemre  43960  nnfoctbdjlem  44000  iundjiun  44005  vonvolmbllem  44205  smfpimcclem  44351  smfsuplem1  44355  f1cof1blem  44579  elbigo  45908  restclsseplem  46219  sepnsepo  46228  aacllem  46516