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 18	1 ⊢ (𝜑 → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-in 3912

This theorem is referenced by:  iinrab2  5034  disji2  5093  disjprg  5105  disjxun  5107  riinint  5962  fnresdisj  6655  fnimadisj  6667  fninfp  7172  ecinxp  8786  fiint  9282  fival  9368  marypha1lem  9389  kmlem12  10141  fin23lem12  10310  fin23lem30  10321  fin23lem33  10324  ttukeylem1  10488  fpwwe2cbv  10610  fpwwe2lem2  10612  fpwwe2  10623  fzval2  13533  fvinim0ffz  13814  limsupval  15521  limsupgval  15523  ello1  15562  elo1  15573  fsum1p  15800  incexclem  15886  fprod1p  16018  smuval2  16535  smueqlem  16543  smumul  16546  setsdm  17225  isacs2  17704  acsfiel  17705  isacs1i  17708  cat1lem  18148  catcval  18152  resscatc  18161  acsficl  18598  lsmdisj3  19748  lsmdisj3a  19754  dprdres  20095  dprdz  20097  dpjdisj  20120  lspdisj2  21251  indistopon  23158  restopnb  23332  ordtrest2  23361  isnrm  23492  cmpcov  23546  cmpsublem  23556  cmpsub  23557  tgcmp  23558  uncmp  23560  hauscmplem  23563  nconnsubb  23580  isnlly  23626  dissnlocfin  23686  kgeni  23694  kgencn3  23715  ptcld  23770  ptcnplem  23778  alexsublem  24201  alexsubb  24203  alexsubALTlem2  24205  alexsubALTlem4  24207  alexsubALT  24208  tmdgsum2  24253  tsmsval2  24287  ustexsym  24373  metrest  24681  qtopbaslem  24915  cnheibor  25114  bndth  25117  lebnumii  25125  iscph  25329  csscld  25408  clsocv  25409  cphsscph  25410  ovolicc2  25681  voliunlem3  25711  ioombl  25724  uniioombllem2  25742  uniioombllem4  25745  uniioombllem6  25747  mbflimsup  25825  taylfval  26522  chtval  27274  ppival  27291  ppival2  27292  ppival2g  27293  chtfl  27313  ppiprm  27315  chtprm  27317  chtnprm  27318  chtdif  27322  ppidif  27327  prmorcht  27342  nosupbnd2lem1  27879  dfprlng3  29198  dfpth2  30078  chdmj2  31882  cmcmlem  31943  pjoml2  31963  fh2  31971  mdbr  32646  mdi  32647  mdbr3  32649  mdbr4  32650  dmdmd  32652  dmdbr3  32657  dmdbr4  32658  dmdi4  32659  dmdbr5  32660  mddmd2  32661  mdsl1i  32673  cvmdi  32676  mdslmd1lem1  32677  mdslmd1lem2  32678  mdslmd1lem3  32679  mdslmd1lem4  32680  mdslmd1i  32681  mdslmd3i  32684  csmdsymi  32686  mdexchi  32687  atomli  32734  atabsi  32753  sumdmdlem2  32771  dmdbr5ati  32774  difuncomp  32898  disji2f  32922  disjif2  32926  disjxpin  32933  disjunsn  32939  fnresin  32969  cycpmco2f1  33444  cycpmconjslem2  33475  locfinreflem  34230  iscref  34234  ordtrest2NEW  34313  ordtconnlem1  34314  carsgclctunlem1  34707  totprobd  34816  probmeasb  34820  ballotlemfval  34880  ballotlemfp1  34882  ballotlemgun  34915  chtvalz  35016  bnj1385  35220  bnj1326  35414  vonf1wev  35592  vonf1owevOLD  35594  iccllysconn  35742  satfv1  35855  mvrsval  35997  mrsubvrs  36014  mpstval  36027  msubvrs  36052  neibastop2lem  36871  neibastop2  36872  neibastop3  36873  limsucncmpi  36956  dfttc4  37041  mh-infprim2bi  37058  bj-ismoore  37747  fvineqsnf1  38056  pibt2  38063  ptrest  38270  mblfinlem2  38309  sstotbnd2  38425  cntotbnd  38447  heibor  38472  xrneq1  39045  disjressuc2  39060  ecqmap  39098  l1cvat  39829  pmodlem2  40621  pmod2iN  40623  hlmod1i  40630  osumcllem3N  40732  osumcllem9N  40738  pexmidlem6N  40749  pl42lem1N  40753  istrnN  40931  djavalN  41909  dihmeetlem9N  42089  dihmeetlem11N  42091  dihmeetlem12N  42092  dihoml4  42151  djhval  42172  dochexmidlem6  42239  lclkrlem2b  42282  lcfrlem20  42336  lcfrlem23  42339  elrfi  43425  isnacs  43435  mrefg2  43438  mapfzcons2  43450  coeq0i  43484  eldioph2lem2  43492  aomclem8  43788  kelac1  43790  islmodfg  43796  lnr2i  43843  fgraphopab  43930  ntrkbimka  44764  ntrk0kbimka  44765  isotone2  44775  ntrclskb  44795  ntrclsk3  44796  ntrclsk13  44797  neicvgbex  44838  disjrnmpt2  45906  disjinfi  45910  uzinico2  46277  uzinico3  46278  fsumiunss  46291  lptre2pt  46354  limsupresre  46410  limsuplesup  46413  limsupresico  46414  limsupvaluz  46422  limsuplt2  46467  liminfval  46473  limsupge  46475  liminfgval  46476  liminfval2  46482  liminfresico  46485  liminflelimsuplem  46489  liminflelimsup  46490  stoweidlem50  46764  stoweidlem57  46771  subsaliuncllem  47071  sge0val  47080  sge0iunmptlemre  47129  nnfoctbdjlem  47169  iundjiun  47174  vonvolmbllem  47374  smfpimcclem  47521  smfsuplem1  47525  f1cof1blem  47811  3f1oss1  47812  grimuhgr  48652  elbigo  49331  restclsseplem  49693  sepnsepo  49702  aacllem  50621