Theorem ineq1d 4168

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-in 3905

This theorem is referenced by:  iinrab2  5022  disji2  5079  disjprg  5091  disjxun  5093  riinint  5918  fnresdisj  6609  fnimadisj  6621  fninfp  7117  ecinxp  8725  fiint  9222  fival  9307  marypha1lem  9328  kmlem12  10064  fin23lem12  10233  fin23lem30  10244  fin23lem33  10247  ttukeylem1  10411  fpwwe2cbv  10532  fpwwe2lem2  10534  fpwwe2  10545  fzval2  13417  fvinim0ffz  13696  limsupval  15388  limsupgval  15390  ello1  15429  elo1  15440  fsum1p  15667  incexclem  15750  fprod1p  15882  smuval2  16400  smueqlem  16408  smumul  16411  setsdm  17088  isacs2  17567  acsfiel  17568  isacs1i  17571  cat1lem  18011  catcval  18015  resscatc  18024  acsficl  18461  lsmdisj3  19603  lsmdisj3a  19609  dprdres  19950  dprdz  19952  dpjdisj  19975  lspdisj2  21073  indistopon  22936  restopnb  23110  ordtrest2  23139  isnrm  23270  cmpcov  23324  cmpsublem  23334  cmpsub  23335  tgcmp  23336  uncmp  23338  hauscmplem  23341  nconnsubb  23358  isnlly  23404  dissnlocfin  23464  kgeni  23472  kgencn3  23493  ptcld  23548  ptcnplem  23556  alexsublem  23979  alexsubb  23981  alexsubALTlem2  23983  alexsubALTlem4  23985  alexsubALT  23986  tmdgsum2  24031  tsmsval2  24065  ustexsym  24151  metrest  24459  qtopbaslem  24693  cnheibor  24901  bndth  24904  lebnumii  24912  iscph  25117  csscld  25196  clsocv  25197  cphsscph  25198  ovolicc2  25470  voliunlem3  25500  ioombl  25513  uniioombllem2  25531  uniioombllem4  25534  uniioombllem6  25536  mbflimsup  25614  taylfval  26313  chtval  27067  ppival  27084  ppival2  27085  ppival2g  27086  chtfl  27106  ppiprm  27108  chtprm  27110  chtnprm  27111  chtdif  27115  ppidif  27120  prmorcht  27135  nosupbnd2lem1  27674  dfpth2  29728  chdmj2  31531  cmcmlem  31592  pjoml2  31612  fh2  31620  mdbr  32295  mdi  32296  mdbr3  32298  mdbr4  32299  dmdmd  32301  dmdbr3  32306  dmdbr4  32307  dmdi4  32308  dmdbr5  32309  mddmd2  32310  mdsl1i  32322  cvmdi  32325  mdslmd1lem1  32326  mdslmd1lem2  32327  mdslmd1lem3  32328  mdslmd1lem4  32329  mdslmd1i  32330  mdslmd3i  32333  csmdsymi  32335  mdexchi  32336  atomli  32383  atabsi  32402  sumdmdlem2  32420  dmdbr5ati  32423  difuncomp  32554  disji2f  32578  disjif2  32582  disjxpin  32589  disjunsn  32595  fnresin  32628  cycpmco2f1  33134  cycpmconjslem2  33165  locfinreflem  33925  iscref  33929  ordtrest2NEW  34008  ordtconnlem1  34009  carsgclctunlem1  34402  totprobd  34511  probmeasb  34515  ballotlemfval  34575  ballotlemfp1  34577  ballotlemgun  34610  chtvalz  34714  bnj1385  34916  bnj1326  35110  vonf1owev  35224  iccllysconn  35366  satfv1  35479  mvrsval  35621  mrsubvrs  35638  mpstval  35651  msubvrs  35676  neibastop2lem  36476  neibastop2  36477  neibastop3  36478  limsucncmpi  36561  bj-ismoore  37222  fvineqsnf1  37527  pibt2  37534  ptrest  37732  mblfinlem2  37771  sstotbnd2  37887  cntotbnd  37909  heibor  37934  xrneq1  38493  disjressuc2  38508  l1cvat  39227  pmodlem2  40019  pmod2iN  40021  hlmod1i  40028  osumcllem3N  40130  osumcllem9N  40136  pexmidlem6N  40147  pl42lem1N  40151  istrnN  40329  djavalN  41307  dihmeetlem9N  41487  dihmeetlem11N  41489  dihmeetlem12N  41490  dihoml4  41549  djhval  41570  dochexmidlem6  41637  lclkrlem2b  41680  lcfrlem20  41734  lcfrlem23  41737  elrfi  42851  isnacs  42861  mrefg2  42864  mapfzcons2  42876  coeq0i  42910  eldioph2lem2  42918  aomclem8  43218  kelac1  43220  islmodfg  43226  lnr2i  43273  fgraphopab  43360  ntrkbimka  44195  ntrk0kbimka  44196  isotone2  44206  ntrclskb  44226  ntrclsk3  44227  ntrclsk13  44228  neicvgbex  44269  disjrnmpt2  45348  disjinfi  45352  uzinico2  45723  uzinico3  45724  fsumiunss  45737  lptre2pt  45800  limsupresre  45856  limsuplesup  45859  limsupresico  45860  limsupvaluz  45868  limsuplt2  45913  liminfval  45919  limsupge  45921  liminfgval  45922  liminfval2  45928  liminfresico  45931  liminflelimsuplem  45935  liminflelimsup  45936  stoweidlem50  46210  stoweidlem57  46217  subsaliuncllem  46517  sge0val  46526  sge0iunmptlemre  46575  nnfoctbdjlem  46615  iundjiun  46620  vonvolmbllem  46820  smfpimcclem  46967  smfsuplem1  46971  f1cof1blem  47236  3f1oss1  47237  grimuhgr  48049  elbigo  48713  restclsseplem  49076  sepnsepo  49085  aacllem  49962