Theorem ineq1d 4182

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

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

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 3406  df-in 3921

This theorem is referenced by:  iinrab2  5034  disji2  5091  disjprg  5103  disjxun  5105  riinint  5935  fnresdisj  6638  fnimadisj  6650  fninfp  7148  ecinxp  8765  fiint  9277  fiintOLD  9278  fival  9363  marypha1lem  9384  kmlem12  10115  fin23lem12  10284  fin23lem30  10295  fin23lem33  10298  ttukeylem1  10462  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2  10596  fzval2  13471  fvinim0ffz  13747  limsupval  15440  limsupgval  15442  ello1  15481  elo1  15492  fsum1p  15719  incexclem  15802  fprod1p  15934  smuval2  16452  smueqlem  16460  smumul  16463  setsdm  17140  isacs2  17614  acsfiel  17615  isacs1i  17618  cat1lem  18058  catcval  18062  resscatc  18071  acsficl  18506  lsmdisj3  19613  lsmdisj3a  19619  dprdres  19960  dprdz  19962  dpjdisj  19985  lspdisj2  21037  indistopon  22888  restopnb  23062  ordtrest2  23091  isnrm  23222  cmpcov  23276  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  hauscmplem  23293  nconnsubb  23310  isnlly  23356  dissnlocfin  23416  kgeni  23424  kgencn3  23445  ptcld  23500  ptcnplem  23508  alexsublem  23931  alexsubb  23933  alexsubALTlem2  23935  alexsubALTlem4  23937  alexsubALT  23938  tmdgsum2  23983  tsmsval2  24017  ustexsym  24103  metrest  24412  qtopbaslem  24646  cnheibor  24854  bndth  24857  lebnumii  24865  iscph  25070  csscld  25149  clsocv  25150  cphsscph  25151  ovolicc2  25423  voliunlem3  25453  ioombl  25466  uniioombllem2  25484  uniioombllem4  25487  uniioombllem6  25489  mbflimsup  25567  taylfval  26266  chtval  27020  ppival  27037  ppival2  27038  ppival2g  27039  chtfl  27059  ppiprm  27061  chtprm  27063  chtnprm  27064  chtdif  27068  ppidif  27073  prmorcht  27088  nosupbnd2lem1  27627  dfpth2  29659  chdmj2  31459  cmcmlem  31520  pjoml2  31540  fh2  31548  mdbr  32223  mdi  32224  mdbr3  32226  mdbr4  32227  dmdmd  32229  dmdbr3  32234  dmdbr4  32235  dmdi4  32236  dmdbr5  32237  mddmd2  32238  mdsl1i  32250  cvmdi  32253  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd1lem3  32256  mdslmd1lem4  32257  mdslmd1i  32258  mdslmd3i  32261  csmdsymi  32263  mdexchi  32264  atomli  32311  atabsi  32330  sumdmdlem2  32348  dmdbr5ati  32351  difuncomp  32482  disji2f  32506  disjif2  32510  disjxpin  32517  disjunsn  32523  fnresin  32550  cycpmco2f1  33081  cycpmconjslem2  33112  locfinreflem  33830  iscref  33834  ordtrest2NEW  33913  ordtconnlem1  33914  carsgclctunlem1  34308  totprobd  34417  probmeasb  34421  ballotlemfval  34481  ballotlemfp1  34483  ballotlemgun  34516  chtvalz  34620  bnj1385  34822  bnj1326  35016  vonf1owev  35095  iccllysconn  35237  satfv1  35350  mvrsval  35492  mrsubvrs  35509  mpstval  35522  msubvrs  35547  neibastop2lem  36348  neibastop2  36349  neibastop3  36350  limsucncmpi  36433  bj-ismoore  37093  fvineqsnf1  37398  pibt2  37405  ptrest  37613  mblfinlem2  37652  sstotbnd2  37768  cntotbnd  37790  heibor  37815  xrneq1  38363  disjressuc2  38374  l1cvat  39048  pmodlem2  39841  pmod2iN  39843  hlmod1i  39850  osumcllem3N  39952  osumcllem9N  39958  pexmidlem6N  39969  pl42lem1N  39973  istrnN  40151  djavalN  41129  dihmeetlem9N  41309  dihmeetlem11N  41311  dihmeetlem12N  41312  dihoml4  41371  djhval  41392  dochexmidlem6  41459  lclkrlem2b  41502  lcfrlem20  41556  lcfrlem23  41559  elrfi  42682  isnacs  42692  mrefg2  42695  mapfzcons2  42707  coeq0i  42741  eldioph2lem2  42749  aomclem8  43050  kelac1  43052  islmodfg  43058  lnr2i  43105  fgraphopab  43192  ntrkbimka  44027  ntrk0kbimka  44028  isotone2  44038  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  neicvgbex  44101  disjrnmpt2  45182  disjinfi  45186  uzinico2  45559  uzinico3  45560  fsumiunss  45573  lptre2pt  45638  limsupresre  45694  limsuplesup  45697  limsupresico  45698  limsupvaluz  45706  limsuplt2  45751  liminfval  45757  limsupge  45759  liminfgval  45760  liminfval2  45766  liminfresico  45769  liminflelimsuplem  45773  liminflelimsup  45774  stoweidlem50  46048  stoweidlem57  46055  subsaliuncllem  46355  sge0val  46364  sge0iunmptlemre  46413  nnfoctbdjlem  46453  iundjiun  46458  vonvolmbllem  46658  smfpimcclem  46805  smfsuplem1  46809  f1cof1blem  47075  3f1oss1  47076  grimuhgr  47887  elbigo  48540  restclsseplem  48903  sepnsepo  48912  aacllem  49790