Theorem ineq1d 4178

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

Syntax hints:   → wi 4   = wceq 1540   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-in 3918

This theorem is referenced by:  iinrab2  5029  disji2  5086  disjprg  5098  disjxun  5100  riinint  5924  fnresdisj  6620  fnimadisj  6632  fninfp  7130  ecinxp  8742  fiint  9253  fiintOLD  9254  fival  9339  marypha1lem  9360  kmlem12  10091  fin23lem12  10260  fin23lem30  10271  fin23lem33  10274  ttukeylem1  10438  fpwwe2cbv  10559  fpwwe2lem2  10561  fpwwe2  10572  fzval2  13447  fvinim0ffz  13723  limsupval  15416  limsupgval  15418  ello1  15457  elo1  15468  fsum1p  15695  incexclem  15778  fprod1p  15910  smuval2  16428  smueqlem  16436  smumul  16439  setsdm  17116  isacs2  17590  acsfiel  17591  isacs1i  17594  cat1lem  18034  catcval  18038  resscatc  18047  acsficl  18482  lsmdisj3  19589  lsmdisj3a  19595  dprdres  19936  dprdz  19938  dpjdisj  19961  lspdisj2  21013  indistopon  22864  restopnb  23038  ordtrest2  23067  isnrm  23198  cmpcov  23252  cmpsublem  23262  cmpsub  23263  tgcmp  23264  uncmp  23266  hauscmplem  23269  nconnsubb  23286  isnlly  23332  dissnlocfin  23392  kgeni  23400  kgencn3  23421  ptcld  23476  ptcnplem  23484  alexsublem  23907  alexsubb  23909  alexsubALTlem2  23911  alexsubALTlem4  23913  alexsubALT  23914  tmdgsum2  23959  tsmsval2  23993  ustexsym  24079  metrest  24388  qtopbaslem  24622  cnheibor  24830  bndth  24833  lebnumii  24841  iscph  25046  csscld  25125  clsocv  25126  cphsscph  25127  ovolicc2  25399  voliunlem3  25429  ioombl  25442  uniioombllem2  25460  uniioombllem4  25463  uniioombllem6  25465  mbflimsup  25543  taylfval  26242  chtval  26996  ppival  27013  ppival2  27014  ppival2g  27015  chtfl  27035  ppiprm  27037  chtprm  27039  chtnprm  27040  chtdif  27044  ppidif  27049  prmorcht  27064  nosupbnd2lem1  27603  dfpth2  29632  chdmj2  31432  cmcmlem  31493  pjoml2  31513  fh2  31521  mdbr  32196  mdi  32197  mdbr3  32199  mdbr4  32200  dmdmd  32202  dmdbr3  32207  dmdbr4  32208  dmdi4  32209  dmdbr5  32210  mddmd2  32211  mdsl1i  32223  cvmdi  32226  mdslmd1lem1  32227  mdslmd1lem2  32228  mdslmd1lem3  32229  mdslmd1lem4  32230  mdslmd1i  32231  mdslmd3i  32234  csmdsymi  32236  mdexchi  32237  atomli  32284  atabsi  32303  sumdmdlem2  32321  dmdbr5ati  32324  difuncomp  32455  disji2f  32479  disjif2  32483  disjxpin  32490  disjunsn  32496  fnresin  32523  cycpmco2f1  33054  cycpmconjslem2  33085  locfinreflem  33803  iscref  33807  ordtrest2NEW  33886  ordtconnlem1  33887  carsgclctunlem1  34281  totprobd  34390  probmeasb  34394  ballotlemfval  34454  ballotlemfp1  34456  ballotlemgun  34489  chtvalz  34593  bnj1385  34795  bnj1326  34989  vonf1owev  35068  iccllysconn  35210  satfv1  35323  mvrsval  35465  mrsubvrs  35482  mpstval  35495  msubvrs  35520  neibastop2lem  36321  neibastop2  36322  neibastop3  36323  limsucncmpi  36406  bj-ismoore  37066  fvineqsnf1  37371  pibt2  37378  ptrest  37586  mblfinlem2  37625  sstotbnd2  37741  cntotbnd  37763  heibor  37788  xrneq1  38336  disjressuc2  38347  l1cvat  39021  pmodlem2  39814  pmod2iN  39816  hlmod1i  39823  osumcllem3N  39925  osumcllem9N  39931  pexmidlem6N  39942  pl42lem1N  39946  istrnN  40124  djavalN  41102  dihmeetlem9N  41282  dihmeetlem11N  41284  dihmeetlem12N  41285  dihoml4  41344  djhval  41365  dochexmidlem6  41432  lclkrlem2b  41475  lcfrlem20  41529  lcfrlem23  41532  elrfi  42655  isnacs  42665  mrefg2  42668  mapfzcons2  42680  coeq0i  42714  eldioph2lem2  42722  aomclem8  43023  kelac1  43025  islmodfg  43031  lnr2i  43078  fgraphopab  43165  ntrkbimka  44000  ntrk0kbimka  44001  isotone2  44011  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  neicvgbex  44074  disjrnmpt2  45155  disjinfi  45159  uzinico2  45532  uzinico3  45533  fsumiunss  45546  lptre2pt  45611  limsupresre  45667  limsuplesup  45670  limsupresico  45671  limsupvaluz  45679  limsuplt2  45724  liminfval  45730  limsupge  45732  liminfgval  45733  liminfval2  45739  liminfresico  45742  liminflelimsuplem  45746  liminflelimsup  45747  stoweidlem50  46021  stoweidlem57  46028  subsaliuncllem  46328  sge0val  46337  sge0iunmptlemre  46386  nnfoctbdjlem  46426  iundjiun  46431  vonvolmbllem  46631  smfpimcclem  46778  smfsuplem1  46782  f1cof1blem  47048  3f1oss1  47049  grimuhgr  47860  elbigo  48513  restclsseplem  48876  sepnsepo  48885  aacllem  49763