Theorem ineq1d 4171

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-in 3908

This theorem is referenced by:  iinrab2  5025  disji2  5082  disjprg  5094  disjxun  5096  riinint  5921  fnresdisj  6612  fnimadisj  6624  fninfp  7120  ecinxp  8729  fiint  9227  fival  9315  marypha1lem  9336  kmlem12  10072  fin23lem12  10241  fin23lem30  10252  fin23lem33  10255  ttukeylem1  10419  fpwwe2cbv  10541  fpwwe2lem2  10543  fpwwe2  10554  fzval2  13426  fvinim0ffz  13705  limsupval  15397  limsupgval  15399  ello1  15438  elo1  15449  fsum1p  15676  incexclem  15759  fprod1p  15891  smuval2  16409  smueqlem  16417  smumul  16420  setsdm  17097  isacs2  17576  acsfiel  17577  isacs1i  17580  cat1lem  18020  catcval  18024  resscatc  18033  acsficl  18470  lsmdisj3  19612  lsmdisj3a  19618  dprdres  19959  dprdz  19961  dpjdisj  19984  lspdisj2  21082  indistopon  22945  restopnb  23119  ordtrest2  23148  isnrm  23279  cmpcov  23333  cmpsublem  23343  cmpsub  23344  tgcmp  23345  uncmp  23347  hauscmplem  23350  nconnsubb  23367  isnlly  23413  dissnlocfin  23473  kgeni  23481  kgencn3  23502  ptcld  23557  ptcnplem  23565  alexsublem  23988  alexsubb  23990  alexsubALTlem2  23992  alexsubALTlem4  23994  alexsubALT  23995  tmdgsum2  24040  tsmsval2  24074  ustexsym  24160  metrest  24468  qtopbaslem  24702  cnheibor  24910  bndth  24913  lebnumii  24921  iscph  25126  csscld  25205  clsocv  25206  cphsscph  25207  ovolicc2  25479  voliunlem3  25509  ioombl  25522  uniioombllem2  25540  uniioombllem4  25543  uniioombllem6  25545  mbflimsup  25623  taylfval  26322  chtval  27076  ppival  27093  ppival2  27094  ppival2g  27095  chtfl  27115  ppiprm  27117  chtprm  27119  chtnprm  27120  chtdif  27124  ppidif  27129  prmorcht  27144  nosupbnd2lem1  27683  dfpth2  29802  chdmj2  31605  cmcmlem  31666  pjoml2  31686  fh2  31694  mdbr  32369  mdi  32370  mdbr3  32372  mdbr4  32373  dmdmd  32375  dmdbr3  32380  dmdbr4  32381  dmdi4  32382  dmdbr5  32383  mddmd2  32384  mdsl1i  32396  cvmdi  32399  mdslmd1lem1  32400  mdslmd1lem2  32401  mdslmd1lem3  32402  mdslmd1lem4  32403  mdslmd1i  32404  mdslmd3i  32407  csmdsymi  32409  mdexchi  32410  atomli  32457  atabsi  32476  sumdmdlem2  32494  dmdbr5ati  32497  difuncomp  32628  disji2f  32652  disjif2  32656  disjxpin  32663  disjunsn  32669  fnresin  32702  cycpmco2f1  33206  cycpmconjslem2  33237  locfinreflem  33997  iscref  34001  ordtrest2NEW  34080  ordtconnlem1  34081  carsgclctunlem1  34474  totprobd  34583  probmeasb  34587  ballotlemfval  34647  ballotlemfp1  34649  ballotlemgun  34682  chtvalz  34786  bnj1385  34988  bnj1326  35182  vonf1owev  35302  iccllysconn  35444  satfv1  35557  mvrsval  35699  mrsubvrs  35716  mpstval  35729  msubvrs  35754  neibastop2lem  36554  neibastop2  36555  neibastop3  36556  limsucncmpi  36639  bj-ismoore  37310  fvineqsnf1  37615  pibt2  37622  ptrest  37820  mblfinlem2  37859  sstotbnd2  37975  cntotbnd  37997  heibor  38022  xrneq1  38581  disjressuc2  38596  l1cvat  39315  pmodlem2  40107  pmod2iN  40109  hlmod1i  40116  osumcllem3N  40218  osumcllem9N  40224  pexmidlem6N  40235  pl42lem1N  40239  istrnN  40417  djavalN  41395  dihmeetlem9N  41575  dihmeetlem11N  41577  dihmeetlem12N  41578  dihoml4  41637  djhval  41658  dochexmidlem6  41725  lclkrlem2b  41768  lcfrlem20  41822  lcfrlem23  41825  elrfi  42936  isnacs  42946  mrefg2  42949  mapfzcons2  42961  coeq0i  42995  eldioph2lem2  43003  aomclem8  43303  kelac1  43305  islmodfg  43311  lnr2i  43358  fgraphopab  43445  ntrkbimka  44279  ntrk0kbimka  44280  isotone2  44290  ntrclskb  44310  ntrclsk3  44311  ntrclsk13  44312  neicvgbex  44353  disjrnmpt2  45432  disjinfi  45436  uzinico2  45807  uzinico3  45808  fsumiunss  45821  lptre2pt  45884  limsupresre  45940  limsuplesup  45943  limsupresico  45944  limsupvaluz  45952  limsuplt2  45997  liminfval  46003  limsupge  46005  liminfgval  46006  liminfval2  46012  liminfresico  46015  liminflelimsuplem  46019  liminflelimsup  46020  stoweidlem50  46294  stoweidlem57  46301  subsaliuncllem  46601  sge0val  46610  sge0iunmptlemre  46659  nnfoctbdjlem  46699  iundjiun  46704  vonvolmbllem  46904  smfpimcclem  47051  smfsuplem1  47055  f1cof1blem  47320  3f1oss1  47321  grimuhgr  48133  elbigo  48797  restclsseplem  49160  sepnsepo  49169  aacllem  50046