Theorem ineq1d 4119

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∩ cin 4092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-in 4094

This theorem is used by:  iinrab2  5033  disji2  5092  disjprg  5104  disjxun  5106  riinint  5966  fnresdisj  6689  fnimadisj  6701  fninfp  7210  ecinxp  8851  fiint  9356  fival  9441  marypha1lem  9462  kmlem12  10279  fin23lem12  10448  fin23lem30  10459  fin23lem33  10462  ttukeylem1  10626  fpwwe2cbv  10754  fpwwe2lem2  10756  fpwwe2  10767  fzval2  13682  fvinim0ffz  13964  limsupval  15685  limsupgval  15687  ello1  15726  elo1  15737  fsum1p  15963  incexclem  16049  fprod1p  16179  smuval2  16696  smueqlem  16704  smumul  16707  setsdm  17392  isacs2  17877  acsfiel  17878  isacs1i  17881  cat1lem  18321  catcval  18325  resscatc  18334  acsficl  18771  lsmdisj3  19948  lsmdisj3a  19954  dprdres  20295  dprdz  20297  dpjdisj  20320  lspdisj2  21456  indistopon  23374  restopnb  23548  ordtrest2  23577  isnrm  23708  cmpcov  23762  cmpsublem  23772  cmpsub  23773  tgcmp  23774  uncmp  23776  hauscmplem  23779  nconnsubb  23796  isnlly  23843  dissnlocfin  23903  kgeni  23911  kgencn3  23932  ptcld  23987  ptcnplem  23995  alexsublem  24418  alexsubb  24420  alexsubALTlem2  24422  alexsubALTlem4  24424  alexsubALT  24425  tmdgsum2  24470  tsmsval2  24504  ustexsym  24590  metrest  24898  qtopbaslem  25132  cnheibor  25331  bndth  25334  lebnumii  25342  iscph  25546  csscld  25625  clsocv  25626  cphsscph  25627  ovolicc2  25898  voliunlem3  25928  ioombl  25941  uniioombllem2  25959  uniioombllem4  25962  uniioombllem6  25964  mbflimsup  26042  taylfval  26743  chtval  27494  ppival  27511  ppival2  27512  ppival2g  27513  chtfl  27533  ppiprm  27535  chtprm  27537  chtnprm  27538  chtdif  27542  ppidif  27547  prmorcht  27562  nosupbnd2lem1  28129  dfprlng3  29483  dfpth2  30371  chdmj2  32189  cmcmlem  32250  pjoml2  32270  fh2  32278  mdbr  32953  mdi  32954  mdbr3  32956  mdbr4  32957  dmdmd  32959  dmdbr3  32964  dmdbr4  32965  dmdi4  32966  dmdbr5  32967  mddmd2  32968  mdsl1i  32980  cvmdi  32983  mdslmd1lem1  32984  mdslmd1lem2  32985  mdslmd1lem3  32986  mdslmd1lem4  32987  mdslmd1i  32988  mdslmd3i  32991  csmdsymi  32993  mdexchi  32994  atomli  33041  atabsi  33060  sumdmdlem2  33078  dmdbr5ati  33081  difuncomp  33246  disji2f  33269  disjif2  33273  disjxpin  33280  disjunsn  33286  fnresin  33316  cycpmco2f1  33784  cycpmconjslem2  33815  locfinreflem  34583  iscref  34587  ordtrest2NEW  34666  ordtconnlem1  34667  carsgclctunlem1  35060  totprobd  35169  probmeasb  35173  ballotlemfval  35233  ballotlemfp1  35235  ballotlemgun  35268  chtvalz  35369  bnj1385  35573  bnj1326  35767  vonf1wev  36077  vonf1owevOLD  36079  iccllysconn  36223  satfv1  36336  mvrsval  36478  mrsubvrs  36495  mpstval  36508  msubvrs  36533  neibastop2lem  37363  neibastop2  37364  neibastop3  37365  limsucncmpi  37448  dfttc4  37533  mh-infprim2bi  37550  bj-ismoore  38296  fvineqsnf1  38601  pibt2  38608  ptrest  38805  mblfinlem2  38844  sstotbnd2  38974  cntotbnd  38996  heibor  39021  xrneq1  39594  disjressuc2  39609  ecqmap  39647  l1cvat  40378  pmodlem2  41170  pmod2iN  41172  hlmod1i  41179  osumcllem3N  41281  osumcllem9N  41287  pexmidlem6N  41298  pl42lem1N  41302  istrnN  41480  djavalN  42458  dihmeetlem9N  42638  dihmeetlem11N  42640  dihmeetlem12N  42641  dihoml4  42700  djhval  42721  dochexmidlem6  42788  lclkrlem2b  42831  lcfrlem20  42885  lcfrlem23  42888  elrfi  43971  isnacs  43981  mrefg2  43984  mapfzcons2  43996  coeq0i  44030  eldioph2lem2  44038  aomclem8  44329  kelac1  44331  islmodfg  44337  lnr2i  44383  fgraphopab  44466  ntrkbimka  45299  ntrk0kbimka  45300  isotone2  45310  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  neicvgbex  45373  disjrnmpt2  46476  disjinfi  46480  uzinico2  46846  uzinico3  46847  fsumiunss  46860  lptre2pt  46923  limsupresre  46979  limsuplesup  46982  limsupresico  46983  limsupvaluz  46991  limsuplt2  47036  liminfval  47042  limsupge  47044  liminfgval  47045  liminfval2  47051  liminfresico  47054  liminflelimsuplem  47058  liminflelimsup  47059  stoweidlem50  47333  stoweidlem57  47340  subsaliuncllem  47640  sge0val  47649  sge0iunmptlemre  47698  nnfoctbdjlem  47738  iundjiun  47743  vonvolmbllem  47943  smfpimcclem  48090  smfsuplem1  48094  f1cof1blem  48417  3f1oss1  48418  grimuhgr  49258  elbigo  49994  restclsseplem  50360  sepnsepo  50369  parhomco2  51091  parhomco  51092  parmapco2  51103  parmapco  51104  aacllem  51367