Theorem ineq1d 4148

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-in 3890

This theorem is referenced by:  iinrab2  4999  disji2  5056  disjprg  5068  disjxun  5070  riinint  5914  fnresdisj  6605  fnimadisj  6617  fninfp  7118  ecinxp  8729  fiint  9227  fival  9315  marypha1lem  9336  kmlem12  10075  fin23lem12  10244  fin23lem30  10255  fin23lem33  10258  ttukeylem1  10422  fpwwe2cbv  10544  fpwwe2lem2  10546  fpwwe2  10557  fzval2  13455  fvinim0ffz  13735  limsupval  15427  limsupgval  15429  ello1  15468  elo1  15479  fsum1p  15706  incexclem  15792  fprod1p  15924  smuval2  16442  smueqlem  16450  smumul  16453  setsdm  17131  isacs2  17610  acsfiel  17611  isacs1i  17614  cat1lem  18054  catcval  18058  resscatc  18067  acsficl  18504  lsmdisj3  19649  lsmdisj3a  19655  dprdres  19996  dprdz  19998  dpjdisj  20021  lspdisj2  21120  indistopon  22984  restopnb  23158  ordtrest2  23187  isnrm  23318  cmpcov  23372  cmpsublem  23382  cmpsub  23383  tgcmp  23384  uncmp  23386  hauscmplem  23389  nconnsubb  23406  isnlly  23452  dissnlocfin  23512  kgeni  23520  kgencn3  23541  ptcld  23596  ptcnplem  23604  alexsublem  24027  alexsubb  24029  alexsubALTlem2  24031  alexsubALTlem4  24033  alexsubALT  24034  tmdgsum2  24079  tsmsval2  24113  ustexsym  24199  metrest  24507  qtopbaslem  24741  cnheibor  24940  bndth  24943  lebnumii  24951  iscph  25155  csscld  25234  clsocv  25235  cphsscph  25236  ovolicc2  25507  voliunlem3  25537  ioombl  25550  uniioombllem2  25568  uniioombllem4  25571  uniioombllem6  25573  mbflimsup  25651  taylfval  26342  chtval  27091  ppival  27108  ppival2  27109  ppival2g  27110  chtfl  27130  ppiprm  27132  chtprm  27134  chtnprm  27135  chtdif  27139  ppidif  27144  prmorcht  27159  nosupbnd2lem1  27697  dfpth2  29815  chdmj2  31619  cmcmlem  31680  pjoml2  31700  fh2  31708  mdbr  32383  mdi  32384  mdbr3  32386  mdbr4  32387  dmdmd  32389  dmdbr3  32394  dmdbr4  32395  dmdi4  32396  dmdbr5  32397  mddmd2  32398  mdsl1i  32410  cvmdi  32413  mdslmd1lem1  32414  mdslmd1lem2  32415  mdslmd1lem3  32416  mdslmd1lem4  32417  mdslmd1i  32418  mdslmd3i  32421  csmdsymi  32423  mdexchi  32424  atomli  32471  atabsi  32490  sumdmdlem2  32508  dmdbr5ati  32511  difuncomp  32642  disji2f  32666  disjif2  32670  disjxpin  32677  disjunsn  32683  fnresin  32716  cycpmco2f1  33205  cycpmconjslem2  33236  locfinreflem  34024  iscref  34028  ordtrest2NEW  34107  ordtconnlem1  34108  carsgclctunlem1  34501  totprobd  34610  probmeasb  34614  ballotlemfval  34674  ballotlemfp1  34676  ballotlemgun  34709  chtvalz  34813  bnj1385  35014  bnj1326  35208  vonf1owev  35336  iccllysconn  35478  satfv1  35591  mvrsval  35733  mrsubvrs  35750  mpstval  35763  msubvrs  35788  neibastop2lem  36588  neibastop2  36589  neibastop3  36590  limsucncmpi  36673  dfttc4  36758  mh-infprim2bi  36775  bj-ismoore  37463  fvineqsnf1  37772  pibt2  37779  ptrest  37986  mblfinlem2  38025  sstotbnd2  38141  cntotbnd  38163  heibor  38188  xrneq1  38763  disjressuc2  38778  ecqmap  38816  l1cvat  39547  pmodlem2  40339  pmod2iN  40341  hlmod1i  40348  osumcllem3N  40450  osumcllem9N  40456  pexmidlem6N  40467  pl42lem1N  40471  istrnN  40649  djavalN  41627  dihmeetlem9N  41807  dihmeetlem11N  41809  dihmeetlem12N  41810  dihoml4  41869  djhval  41890  dochexmidlem6  41957  lclkrlem2b  42000  lcfrlem20  42054  lcfrlem23  42057  elrfi  43143  isnacs  43153  mrefg2  43156  mapfzcons2  43168  coeq0i  43202  eldioph2lem2  43210  aomclem8  43506  kelac1  43508  islmodfg  43514  lnr2i  43561  fgraphopab  43648  ntrkbimka  44482  ntrk0kbimka  44483  isotone2  44493  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  neicvgbex  44556  disjrnmpt2  45635  disjinfi  45639  uzinico2  46006  uzinico3  46007  fsumiunss  46020  lptre2pt  46083  limsupresre  46139  limsuplesup  46142  limsupresico  46143  limsupvaluz  46151  limsuplt2  46196  liminfval  46202  limsupge  46204  liminfgval  46205  liminfval2  46211  liminfresico  46214  liminflelimsuplem  46218  liminflelimsup  46219  stoweidlem50  46493  stoweidlem57  46500  subsaliuncllem  46800  sge0val  46809  sge0iunmptlemre  46858  nnfoctbdjlem  46898  iundjiun  46903  vonvolmbllem  47103  smfpimcclem  47250  smfsuplem1  47254  f1cof1blem  47537  3f1oss1  47538  grimuhgr  48378  elbigo  49042  restclsseplem  49405  sepnsepo  49414  aacllem  50291