Theorem ineq1d 4199

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-in 3938

This theorem is referenced by:  iinrab2  5051  disji2  5108  disjprg  5120  disjxun  5122  riinint  5956  fnresdisj  6663  fnimadisj  6675  fninfp  7171  ecinxp  8811  fiint  9343  fiintOLD  9344  fival  9429  marypha1lem  9450  kmlem12  10181  fin23lem12  10350  fin23lem30  10361  fin23lem33  10364  ttukeylem1  10528  fpwwe2cbv  10649  fpwwe2lem2  10651  fpwwe2  10662  fzval2  13532  fvinim0ffz  13807  limsupval  15495  limsupgval  15497  ello1  15536  elo1  15547  fsum1p  15774  incexclem  15857  fprod1p  15989  smuval2  16506  smueqlem  16514  smumul  16517  setsdm  17194  isacs2  17670  acsfiel  17671  isacs1i  17674  cat1lem  18114  catcval  18118  resscatc  18127  acsficl  18562  lsmdisj3  19669  lsmdisj3a  19675  dprdres  20016  dprdz  20018  dpjdisj  20041  lspdisj2  21093  indistopon  22944  restopnb  23118  ordtrest2  23147  isnrm  23278  cmpcov  23332  cmpsublem  23342  cmpsub  23343  tgcmp  23344  uncmp  23346  hauscmplem  23349  nconnsubb  23366  isnlly  23412  dissnlocfin  23472  kgeni  23480  kgencn3  23501  ptcld  23556  ptcnplem  23564  alexsublem  23987  alexsubb  23989  alexsubALTlem2  23991  alexsubALTlem4  23993  alexsubALT  23994  tmdgsum2  24039  tsmsval2  24073  ustexsym  24159  metrest  24468  qtopbaslem  24702  cnheibor  24910  bndth  24913  lebnumii  24921  iscph  25127  csscld  25206  clsocv  25207  cphsscph  25208  ovolicc2  25480  voliunlem3  25510  ioombl  25523  uniioombllem2  25541  uniioombllem4  25544  uniioombllem6  25546  mbflimsup  25624  taylfval  26323  chtval  27077  ppival  27094  ppival2  27095  ppival2g  27096  chtfl  27116  ppiprm  27118  chtprm  27120  chtnprm  27121  chtdif  27125  ppidif  27130  prmorcht  27145  nosupbnd2lem1  27684  dfpth2  29716  chdmj2  31516  cmcmlem  31577  pjoml2  31597  fh2  31605  mdbr  32280  mdi  32281  mdbr3  32283  mdbr4  32284  dmdmd  32286  dmdbr3  32291  dmdbr4  32292  dmdi4  32293  dmdbr5  32294  mddmd2  32295  mdsl1i  32307  cvmdi  32310  mdslmd1lem1  32311  mdslmd1lem2  32312  mdslmd1lem3  32313  mdslmd1lem4  32314  mdslmd1i  32315  mdslmd3i  32318  csmdsymi  32320  mdexchi  32321  atomli  32368  atabsi  32387  sumdmdlem2  32405  dmdbr5ati  32408  difuncomp  32539  disji2f  32563  disjif2  32567  disjxpin  32574  disjunsn  32580  fnresin  32609  cycpmco2f1  33140  cycpmconjslem2  33171  locfinreflem  33876  iscref  33880  ordtrest2NEW  33959  ordtconnlem1  33960  carsgclctunlem1  34354  totprobd  34463  probmeasb  34467  ballotlemfval  34527  ballotlemfp1  34529  ballotlemgun  34562  chtvalz  34666  bnj1385  34868  bnj1326  35062  iccllysconn  35277  satfv1  35390  mvrsval  35532  mrsubvrs  35549  mpstval  35562  msubvrs  35587  neibastop2lem  36383  neibastop2  36384  neibastop3  36385  limsucncmpi  36468  bj-ismoore  37128  fvineqsnf1  37433  pibt2  37440  ptrest  37648  mblfinlem2  37687  sstotbnd2  37803  cntotbnd  37825  heibor  37850  xrneq1  38400  disjressuc2  38411  l1cvat  39078  pmodlem2  39871  pmod2iN  39873  hlmod1i  39880  osumcllem3N  39982  osumcllem9N  39988  pexmidlem6N  39999  pl42lem1N  40003  istrnN  40181  djavalN  41159  dihmeetlem9N  41339  dihmeetlem11N  41341  dihmeetlem12N  41342  dihoml4  41401  djhval  41422  dochexmidlem6  41489  lclkrlem2b  41532  lcfrlem20  41586  lcfrlem23  41589  elrfi  42692  isnacs  42702  mrefg2  42705  mapfzcons2  42717  coeq0i  42751  eldioph2lem2  42759  aomclem8  43060  kelac1  43062  islmodfg  43068  lnr2i  43115  fgraphopab  43202  ntrkbimka  44037  ntrk0kbimka  44038  isotone2  44048  ntrclskb  44068  ntrclsk3  44069  ntrclsk13  44070  neicvgbex  44111  disjrnmpt2  45192  disjinfi  45196  uzinico2  45570  uzinico3  45571  fsumiunss  45584  lptre2pt  45649  limsupresre  45705  limsuplesup  45708  limsupresico  45709  limsupvaluz  45717  limsuplt2  45762  liminfval  45768  limsupge  45770  liminfgval  45771  liminfval2  45777  liminfresico  45780  liminflelimsuplem  45784  liminflelimsup  45785  stoweidlem50  46059  stoweidlem57  46066  subsaliuncllem  46366  sge0val  46375  sge0iunmptlemre  46424  nnfoctbdjlem  46464  iundjiun  46469  vonvolmbllem  46669  smfpimcclem  46816  smfsuplem1  46820  f1cof1blem  47083  3f1oss1  47084  grimuhgr  47880  elbigo  48511  restclsseplem  48869  sepnsepo  48878  aacllem  49645