Theorem ineq1d 4173

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3902

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 3402  df-in 3910

This theorem is referenced by:  iinrab2  5027  disji2  5084  disjprg  5096  disjxun  5098  riinint  5929  fnresdisj  6620  fnimadisj  6632  fninfp  7130  ecinxp  8741  fiint  9239  fival  9327  marypha1lem  9348  kmlem12  10084  fin23lem12  10253  fin23lem30  10264  fin23lem33  10267  ttukeylem1  10431  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2  10566  fzval2  13438  fvinim0ffz  13717  limsupval  15409  limsupgval  15411  ello1  15450  elo1  15461  fsum1p  15688  incexclem  15771  fprod1p  15903  smuval2  16421  smueqlem  16429  smumul  16432  setsdm  17109  isacs2  17588  acsfiel  17589  isacs1i  17592  cat1lem  18032  catcval  18036  resscatc  18045  acsficl  18482  lsmdisj3  19624  lsmdisj3a  19630  dprdres  19971  dprdz  19973  dpjdisj  19996  lspdisj2  21094  indistopon  22957  restopnb  23131  ordtrest2  23160  isnrm  23291  cmpcov  23345  cmpsublem  23355  cmpsub  23356  tgcmp  23357  uncmp  23359  hauscmplem  23362  nconnsubb  23379  isnlly  23425  dissnlocfin  23485  kgeni  23493  kgencn3  23514  ptcld  23569  ptcnplem  23577  alexsublem  24000  alexsubb  24002  alexsubALTlem2  24004  alexsubALTlem4  24006  alexsubALT  24007  tmdgsum2  24052  tsmsval2  24086  ustexsym  24172  metrest  24480  qtopbaslem  24714  cnheibor  24922  bndth  24925  lebnumii  24933  iscph  25138  csscld  25217  clsocv  25218  cphsscph  25219  ovolicc2  25491  voliunlem3  25521  ioombl  25534  uniioombllem2  25552  uniioombllem4  25555  uniioombllem6  25557  mbflimsup  25635  taylfval  26334  chtval  27088  ppival  27105  ppival2  27106  ppival2g  27107  chtfl  27127  ppiprm  27129  chtprm  27131  chtnprm  27132  chtdif  27136  ppidif  27141  prmorcht  27156  nosupbnd2lem1  27695  dfpth2  29814  chdmj2  31618  cmcmlem  31679  pjoml2  31699  fh2  31707  mdbr  32382  mdi  32383  mdbr3  32385  mdbr4  32386  dmdmd  32388  dmdbr3  32393  dmdbr4  32394  dmdi4  32395  dmdbr5  32396  mddmd2  32397  mdsl1i  32409  cvmdi  32412  mdslmd1lem1  32413  mdslmd1lem2  32414  mdslmd1lem3  32415  mdslmd1lem4  32416  mdslmd1i  32417  mdslmd3i  32420  csmdsymi  32422  mdexchi  32423  atomli  32470  atabsi  32489  sumdmdlem2  32507  dmdbr5ati  32510  difuncomp  32640  disji2f  32664  disjif2  32668  disjxpin  32675  disjunsn  32681  fnresin  32714  cycpmco2f1  33218  cycpmconjslem2  33249  locfinreflem  34018  iscref  34022  ordtrest2NEW  34101  ordtconnlem1  34102  carsgclctunlem1  34495  totprobd  34604  probmeasb  34608  ballotlemfval  34668  ballotlemfp1  34670  ballotlemgun  34703  chtvalz  34807  bnj1385  35008  bnj1326  35202  vonf1owev  35324  iccllysconn  35466  satfv1  35579  mvrsval  35721  mrsubvrs  35738  mpstval  35751  msubvrs  35776  neibastop2lem  36576  neibastop2  36577  neibastop3  36578  limsucncmpi  36661  bj-ismoore  37358  fvineqsnf1  37665  pibt2  37672  ptrest  37870  mblfinlem2  37909  sstotbnd2  38025  cntotbnd  38047  heibor  38072  xrneq1  38647  disjressuc2  38662  ecqmap  38700  l1cvat  39431  pmodlem2  40223  pmod2iN  40225  hlmod1i  40232  osumcllem3N  40334  osumcllem9N  40340  pexmidlem6N  40351  pl42lem1N  40355  istrnN  40533  djavalN  41511  dihmeetlem9N  41691  dihmeetlem11N  41693  dihmeetlem12N  41694  dihoml4  41753  djhval  41774  dochexmidlem6  41841  lclkrlem2b  41884  lcfrlem20  41938  lcfrlem23  41941  elrfi  43051  isnacs  43061  mrefg2  43064  mapfzcons2  43076  coeq0i  43110  eldioph2lem2  43118  aomclem8  43418  kelac1  43420  islmodfg  43426  lnr2i  43473  fgraphopab  43560  ntrkbimka  44394  ntrk0kbimka  44395  isotone2  44405  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  neicvgbex  44468  disjrnmpt2  45547  disjinfi  45551  uzinico2  45921  uzinico3  45922  fsumiunss  45935  lptre2pt  45998  limsupresre  46054  limsuplesup  46057  limsupresico  46058  limsupvaluz  46066  limsuplt2  46111  liminfval  46117  limsupge  46119  liminfgval  46120  liminfval2  46126  liminfresico  46129  liminflelimsuplem  46133  liminflelimsup  46134  stoweidlem50  46408  stoweidlem57  46415  subsaliuncllem  46715  sge0val  46724  sge0iunmptlemre  46773  nnfoctbdjlem  46813  iundjiun  46818  vonvolmbllem  47018  smfpimcclem  47165  smfsuplem1  47169  f1cof1blem  47434  3f1oss1  47435  grimuhgr  48247  elbigo  48911  restclsseplem  49274  sepnsepo  49283  aacllem  50160