Theorem ineq1d 4160

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

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

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 3391  df-in 3897

This theorem is referenced by:  iinrab2  5013  disji2  5070  disjprg  5082  disjxun  5084  riinint  5921  fnresdisj  6612  fnimadisj  6624  fninfp  7122  ecinxp  8732  fiint  9230  fival  9318  marypha1lem  9339  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  21117  indistopon  22976  restopnb  23150  ordtrest2  23179  isnrm  23310  cmpcov  23364  cmpsublem  23374  cmpsub  23375  tgcmp  23376  uncmp  23378  hauscmplem  23381  nconnsubb  23398  isnlly  23444  dissnlocfin  23504  kgeni  23512  kgencn3  23533  ptcld  23588  ptcnplem  23596  alexsublem  24019  alexsubb  24021  alexsubALTlem2  24023  alexsubALTlem4  24025  alexsubALT  24026  tmdgsum2  24071  tsmsval2  24105  ustexsym  24191  metrest  24499  qtopbaslem  24733  cnheibor  24932  bndth  24935  lebnumii  24943  iscph  25147  csscld  25226  clsocv  25227  cphsscph  25228  ovolicc2  25499  voliunlem3  25529  ioombl  25542  uniioombllem2  25560  uniioombllem4  25563  uniioombllem6  25565  mbflimsup  25643  taylfval  26335  chtval  27087  ppival  27104  ppival2  27105  ppival2g  27106  chtfl  27126  ppiprm  27128  chtprm  27130  chtnprm  27131  chtdif  27135  ppidif  27140  prmorcht  27155  nosupbnd2lem1  27693  dfpth2  29812  chdmj2  31616  cmcmlem  31677  pjoml2  31697  fh2  31705  mdbr  32380  mdi  32381  mdbr3  32383  mdbr4  32384  dmdmd  32386  dmdbr3  32391  dmdbr4  32392  dmdi4  32393  dmdbr5  32394  mddmd2  32395  mdsl1i  32407  cvmdi  32410  mdslmd1lem1  32411  mdslmd1lem2  32412  mdslmd1lem3  32413  mdslmd1lem4  32414  mdslmd1i  32415  mdslmd3i  32418  csmdsymi  32420  mdexchi  32421  atomli  32468  atabsi  32487  sumdmdlem2  32505  dmdbr5ati  32508  difuncomp  32638  disji2f  32662  disjif2  32666  disjxpin  32673  disjunsn  32679  fnresin  32712  cycpmco2f1  33200  cycpmconjslem2  33231  locfinreflem  34000  iscref  34004  ordtrest2NEW  34083  ordtconnlem1  34084  carsgclctunlem1  34477  totprobd  34586  probmeasb  34590  ballotlemfval  34650  ballotlemfp1  34652  ballotlemgun  34685  chtvalz  34789  bnj1385  34990  bnj1326  35184  vonf1owev  35306  iccllysconn  35448  satfv1  35561  mvrsval  35703  mrsubvrs  35720  mpstval  35733  msubvrs  35758  neibastop2lem  36558  neibastop2  36559  neibastop3  36560  limsucncmpi  36643  dfttc4  36728  mh-infprim2bi  36745  bj-ismoore  37433  fvineqsnf1  37740  pibt2  37747  ptrest  37954  mblfinlem2  37993  sstotbnd2  38109  cntotbnd  38131  heibor  38156  xrneq1  38731  disjressuc2  38746  ecqmap  38784  l1cvat  39515  pmodlem2  40307  pmod2iN  40309  hlmod1i  40316  osumcllem3N  40418  osumcllem9N  40424  pexmidlem6N  40435  pl42lem1N  40439  istrnN  40617  djavalN  41595  dihmeetlem9N  41775  dihmeetlem11N  41777  dihmeetlem12N  41778  dihoml4  41837  djhval  41858  dochexmidlem6  41925  lclkrlem2b  41968  lcfrlem20  42022  lcfrlem23  42025  elrfi  43140  isnacs  43150  mrefg2  43153  mapfzcons2  43165  coeq0i  43199  eldioph2lem2  43207  aomclem8  43507  kelac1  43509  islmodfg  43515  lnr2i  43562  fgraphopab  43649  ntrkbimka  44483  ntrk0kbimka  44484  isotone2  44494  ntrclskb  44514  ntrclsk3  44515  ntrclsk13  44516  neicvgbex  44557  disjrnmpt2  45636  disjinfi  45640  uzinico2  46009  uzinico3  46010  fsumiunss  46023  lptre2pt  46086  limsupresre  46142  limsuplesup  46145  limsupresico  46146  limsupvaluz  46154  limsuplt2  46199  liminfval  46205  limsupge  46207  liminfgval  46208  liminfval2  46214  liminfresico  46217  liminflelimsuplem  46221  liminflelimsup  46222  stoweidlem50  46496  stoweidlem57  46503  subsaliuncllem  46803  sge0val  46812  sge0iunmptlemre  46861  nnfoctbdjlem  46901  iundjiun  46906  vonvolmbllem  47106  smfpimcclem  47253  smfsuplem1  47257  f1cof1blem  47534  3f1oss1  47535  grimuhgr  48375  elbigo  49039  restclsseplem  49402  sepnsepo  49411  aacllem  50288