Theorem ineq1d 4115

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-in 4090

This theorem is used by:  iinrab2  5027  disji2  5086  disjprg  5098  disjxun  5100  riinint  5954  fnresdisj  6662  fnimadisj  6674  fninfp  7181  ecinxp  8818  fiint  9323  fival  9409  marypha1lem  9430  kmlem12  10245  fin23lem12  10414  fin23lem30  10425  fin23lem33  10428  ttukeylem1  10592  fpwwe2cbv  10720  fpwwe2lem2  10722  fpwwe2  10733  fzval2  13647  fvinim0ffz  13929  limsupval  15648  limsupgval  15650  ello1  15689  elo1  15700  fsum1p  15926  incexclem  16012  fprod1p  16142  smuval2  16659  smueqlem  16667  smumul  16670  setsdm  17355  isacs2  17834  acsfiel  17835  isacs1i  17838  cat1lem  18278  catcval  18282  resscatc  18291  acsficl  18728  lsmdisj3  19904  lsmdisj3a  19910  dprdres  20251  dprdz  20253  dpjdisj  20276  lspdisj2  21412  indistopon  23326  restopnb  23500  ordtrest2  23529  isnrm  23660  cmpcov  23714  cmpsublem  23724  cmpsub  23725  tgcmp  23726  uncmp  23728  hauscmplem  23731  nconnsubb  23748  isnlly  23795  dissnlocfin  23855  kgeni  23863  kgencn3  23884  ptcld  23939  ptcnplem  23947  alexsublem  24370  alexsubb  24372  alexsubALTlem2  24374  alexsubALTlem4  24376  alexsubALT  24377  tmdgsum2  24422  tsmsval2  24456  ustexsym  24542  metrest  24850  qtopbaslem  25084  cnheibor  25283  bndth  25286  lebnumii  25294  iscph  25498  csscld  25577  clsocv  25578  cphsscph  25579  ovolicc2  25850  voliunlem3  25880  ioombl  25893  uniioombllem2  25911  uniioombllem4  25914  uniioombllem6  25916  mbflimsup  25994  taylfval  26693  chtval  27444  ppival  27461  ppival2  27462  ppival2g  27463  chtfl  27483  ppiprm  27485  chtprm  27487  chtnprm  27488  chtdif  27492  ppidif  27497  prmorcht  27512  nosupbnd2lem1  28079  dfprlng3  29433  dfpth2  30321  chdmj2  32139  cmcmlem  32200  pjoml2  32220  fh2  32228  mdbr  32903  mdi  32904  mdbr3  32906  mdbr4  32907  dmdmd  32909  dmdbr3  32914  dmdbr4  32915  dmdi4  32916  dmdbr5  32917  mddmd2  32918  mdsl1i  32930  cvmdi  32933  mdslmd1lem1  32934  mdslmd1lem2  32935  mdslmd1lem3  32936  mdslmd1lem4  32937  mdslmd1i  32938  mdslmd3i  32941  csmdsymi  32943  mdexchi  32944  atomli  32991  atabsi  33010  sumdmdlem2  33028  dmdbr5ati  33031  difuncomp  33197  disji2f  33220  disjif2  33224  disjxpin  33231  disjunsn  33237  fnresin  33267  cycpmco2f1  33733  cycpmconjslem2  33764  locfinreflem  34520  iscref  34524  ordtrest2NEW  34603  ordtconnlem1  34604  carsgclctunlem1  34997  totprobd  35106  probmeasb  35110  ballotlemfval  35170  ballotlemfp1  35172  ballotlemgun  35205  chtvalz  35306  bnj1385  35510  bnj1326  35704  vonf1wev  35957  vonf1owevOLD  35959  iccllysconn  36103  satfv1  36216  mvrsval  36358  mrsubvrs  36375  mpstval  36388  msubvrs  36413  neibastop2lem  37242  neibastop2  37243  neibastop3  37244  limsucncmpi  37327  dfttc4  37412  mh-infprim2bi  37429  bj-ismoore  38132  fvineqsnf1  38440  pibt2  38447  ptrest  38644  mblfinlem2  38683  sstotbnd2  38815  cntotbnd  38837  heibor  38862  xrneq1  39435  disjressuc2  39450  ecqmap  39488  l1cvat  40219  pmodlem2  41011  pmod2iN  41013  hlmod1i  41020  osumcllem3N  41122  osumcllem9N  41128  pexmidlem6N  41139  pl42lem1N  41143  istrnN  41321  djavalN  42299  dihmeetlem9N  42479  dihmeetlem11N  42481  dihmeetlem12N  42482  dihoml4  42541  djhval  42562  dochexmidlem6  42629  lclkrlem2b  42672  lcfrlem20  42726  lcfrlem23  42729  elrfi  43812  isnacs  43822  mrefg2  43825  mapfzcons2  43837  coeq0i  43871  eldioph2lem2  43879  aomclem8  44170  kelac1  44172  islmodfg  44178  lnr2i  44225  fgraphopab  44312  ntrkbimka  45145  ntrk0kbimka  45146  isotone2  45156  ntrclskb  45176  ntrclsk3  45177  ntrclsk13  45178  neicvgbex  45219  disjrnmpt2  46310  disjinfi  46314  uzinico2  46680  uzinico3  46681  fsumiunss  46694  lptre2pt  46757  limsupresre  46813  limsuplesup  46816  limsupresico  46817  limsupvaluz  46825  limsuplt2  46870  liminfval  46876  limsupge  46878  liminfgval  46879  liminfval2  46885  liminfresico  46888  liminflelimsuplem  46892  liminflelimsup  46893  stoweidlem50  47167  stoweidlem57  47174  subsaliuncllem  47474  sge0val  47483  sge0iunmptlemre  47532  nnfoctbdjlem  47572  iundjiun  47577  vonvolmbllem  47777  smfpimcclem  47924  smfsuplem1  47928  f1cof1blem  48251  3f1oss1  48252  grimuhgr  49092  elbigo  49770  restclsseplem  50136  sepnsepo  50145  parhomco2  50867  parhomco  50868  parmapco2  50879  parmapco  50880  aacllem  51121