Theorem ineq1d 4240

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

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-in 3983

This theorem is referenced by:  iinrab2  5093  disji2  5150  disjprg  5162  disjxun  5164  riinint  5994  fnresdisj  6700  fnimadisj  6712  fninfp  7208  ecinxp  8850  fiint  9394  fiintOLD  9395  fival  9481  marypha1lem  9502  kmlem12  10231  fin23lem12  10400  fin23lem30  10411  fin23lem33  10414  ttukeylem1  10578  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwe2  10712  fzval2  13570  fvinim0ffz  13836  limsupval  15520  limsupgval  15522  ello1  15561  elo1  15572  fsum1p  15801  incexclem  15884  fprod1p  16016  smuval2  16528  smueqlem  16536  smumul  16539  setsdm  17217  isacs2  17711  acsfiel  17712  isacs1i  17715  cat1lem  18163  catcval  18167  resscatc  18176  acsficl  18617  lsmdisj3  19725  lsmdisj3a  19731  dprdres  20072  dprdz  20074  dpjdisj  20097  lspdisj2  21152  indistopon  23029  restopnb  23204  ordtrest2  23233  isnrm  23364  cmpcov  23418  cmpsublem  23428  cmpsub  23429  tgcmp  23430  uncmp  23432  hauscmplem  23435  nconnsubb  23452  isnlly  23498  dissnlocfin  23558  kgeni  23566  kgencn3  23587  ptcld  23642  ptcnplem  23650  alexsublem  24073  alexsubb  24075  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  tmdgsum2  24125  tsmsval2  24159  ustexsym  24245  metrest  24558  qtopbaslem  24800  cnheibor  25006  bndth  25009  lebnumii  25017  iscph  25223  csscld  25302  clsocv  25303  cphsscph  25304  ovolicc2  25576  voliunlem3  25606  ioombl  25619  uniioombllem2  25637  uniioombllem4  25640  uniioombllem6  25642  mbflimsup  25720  taylfval  26418  chtval  27171  ppival  27188  ppival2  27189  ppival2g  27190  chtfl  27210  ppiprm  27212  chtprm  27214  chtnprm  27215  chtdif  27219  ppidif  27224  prmorcht  27239  nosupbnd2lem1  27778  chdmj2  31562  cmcmlem  31623  pjoml2  31643  fh2  31651  mdbr  32326  mdi  32327  mdbr3  32329  mdbr4  32330  dmdmd  32332  dmdbr3  32337  dmdbr4  32338  dmdi4  32339  dmdbr5  32340  mddmd2  32341  mdsl1i  32353  cvmdi  32356  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd1lem3  32359  mdslmd1lem4  32360  mdslmd1i  32361  mdslmd3i  32364  csmdsymi  32366  mdexchi  32367  atomli  32414  atabsi  32433  sumdmdlem2  32451  dmdbr5ati  32454  difuncomp  32576  disji2f  32599  disjif2  32603  disjxpin  32610  disjunsn  32616  fnresin  32645  cycpmco2f1  33117  cycpmconjslem2  33148  locfinreflem  33786  iscref  33790  ordtrest2NEW  33869  ordtconnlem1  33870  carsgclctunlem1  34282  totprobd  34391  probmeasb  34395  ballotlemfval  34454  ballotlemfp1  34456  ballotlemgun  34489  chtvalz  34606  bnj1385  34808  bnj1326  35002  iccllysconn  35218  satfv1  35331  mvrsval  35473  mrsubvrs  35490  mpstval  35503  msubvrs  35528  neibastop2lem  36326  neibastop2  36327  neibastop3  36328  limsucncmpi  36411  bj-ismoore  37071  fvineqsnf1  37376  pibt2  37383  ptrest  37579  mblfinlem2  37618  sstotbnd2  37734  cntotbnd  37756  heibor  37781  xrneq1  38333  disjressuc2  38344  l1cvat  39011  pmodlem2  39804  pmod2iN  39806  hlmod1i  39813  osumcllem3N  39915  osumcllem9N  39921  pexmidlem6N  39932  pl42lem1N  39936  istrnN  40114  djavalN  41092  dihmeetlem9N  41272  dihmeetlem11N  41274  dihmeetlem12N  41275  dihoml4  41334  djhval  41355  dochexmidlem6  41422  lclkrlem2b  41465  lcfrlem20  41519  lcfrlem23  41522  metakunt20  42181  elrfi  42650  isnacs  42660  mrefg2  42663  mapfzcons2  42675  coeq0i  42709  eldioph2lem2  42717  aomclem8  43018  kelac1  43020  islmodfg  43026  lnr2i  43073  fgraphopab  43164  ntrkbimka  44000  ntrk0kbimka  44001  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  neicvgbex  44074  disjrnmpt2  45095  disjinfi  45099  uzinico2  45480  uzinico3  45481  fsumiunss  45496  lptre2pt  45561  limsupresre  45617  limsuplesup  45620  limsupresico  45621  limsupvaluz  45629  limsuplt2  45674  liminfval  45680  limsupge  45682  liminfgval  45683  liminfval2  45689  liminfresico  45692  liminflelimsuplem  45696  liminflelimsup  45697  stoweidlem50  45971  stoweidlem57  45978  subsaliuncllem  46278  sge0val  46287  sge0iunmptlemre  46336  nnfoctbdjlem  46376  iundjiun  46381  vonvolmbllem  46581  smfpimcclem  46728  smfsuplem1  46732  f1cof1blem  46989  3f1oss1  46990  grimuhgr  47762  elbigo  48285  restclsseplem  48594  sepnsepo  48603  aacllem  48895