Theorem ineq1d 4158

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-in 3905

This theorem is referenced by:  iinrab2  5017  disji2  5074  disjprgw  5087  disjprg  5088  disjxun  5090  riinint  5909  fnresdisj  6604  fnimadisj  6616  fninfp  7102  ecinxp  8652  fiint  9189  fival  9269  marypha1lem  9290  kmlem12  10018  fin23lem12  10188  fin23lem30  10199  fin23lem33  10202  ttukeylem1  10366  fpwwe2cbv  10487  fpwwe2lem2  10489  fpwwe2  10500  fzval2  13343  fvinim0ffz  13607  limsupval  15282  limsupgval  15284  ello1  15323  elo1  15334  fsum1p  15564  incexclem  15647  fprod1p  15777  smuval2  16288  smueqlem  16296  smumul  16299  setsdm  16968  isacs2  17459  acsfiel  17460  isacs1i  17463  cat1lem  17908  catcval  17912  resscatc  17921  acsficl  18362  lsmdisj3  19384  lsmdisj3a  19390  dprdres  19726  dprdz  19728  dpjdisj  19751  lspdisj2  20495  indistopon  22257  restopnb  22432  ordtrest2  22461  isnrm  22592  cmpcov  22646  cmpsublem  22656  cmpsub  22657  tgcmp  22658  uncmp  22660  hauscmplem  22663  nconnsubb  22680  isnlly  22726  dissnlocfin  22786  kgeni  22794  kgencn3  22815  ptcld  22870  ptcnplem  22878  alexsublem  23301  alexsubb  23303  alexsubALTlem2  23305  alexsubALTlem4  23307  alexsubALT  23308  tmdgsum2  23353  tsmsval2  23387  ustexsym  23473  metrest  23786  qtopbaslem  24028  cnheibor  24224  bndth  24227  lebnumii  24235  iscph  24440  csscld  24519  clsocv  24520  cphsscph  24521  ovolicc2  24792  voliunlem3  24822  ioombl  24835  uniioombllem2  24853  uniioombllem4  24856  uniioombllem6  24858  mbflimsup  24936  taylfval  25624  chtval  26365  ppival  26382  ppival2  26383  ppival2g  26384  chtfl  26404  ppiprm  26406  chtprm  26408  chtnprm  26409  chtdif  26413  ppidif  26418  prmorcht  26433  nosupbnd2lem1  26969  chdmj2  30180  cmcmlem  30241  pjoml2  30261  fh2  30269  mdbr  30944  mdi  30945  mdbr3  30947  mdbr4  30948  dmdmd  30950  dmdbr3  30955  dmdbr4  30956  dmdi4  30957  dmdbr5  30958  mddmd2  30959  mdsl1i  30971  cvmdi  30974  mdslmd1lem1  30975  mdslmd1lem2  30976  mdslmd1lem3  30977  mdslmd1lem4  30978  mdslmd1i  30979  mdslmd3i  30982  csmdsymi  30984  mdexchi  30985  atomli  31032  atabsi  31051  sumdmdlem2  31069  dmdbr5ati  31072  difuncomp  31180  disji2f  31203  disjif2  31207  disjxpin  31214  disjunsn  31220  fnresin  31248  cycpmco2f1  31678  cycpmconjslem2  31709  locfinreflem  32088  iscref  32092  ordtrest2NEW  32171  ordtconnlem1  32172  carsgclctunlem1  32584  totprobd  32693  probmeasb  32697  ballotlemfval  32756  ballotlemfp1  32758  ballotlemgun  32791  chtvalz  32909  bnj1385  33111  bnj1326  33305  iccllysconn  33511  satfv1  33624  mvrsval  33766  mrsubvrs  33783  mpstval  33796  msubvrs  33821  neibastop2lem  34645  neibastop2  34646  neibastop3  34647  limsucncmpi  34730  bj-ismoore  35381  fvineqsnf1  35686  pibt2  35693  ptrest  35881  mblfinlem2  35920  sstotbnd2  36037  cntotbnd  36059  heibor  36084  xrneq1  36644  disjressuc2  36655  l1cvat  37322  pmodlem2  38115  pmod2iN  38117  hlmod1i  38124  osumcllem3N  38226  osumcllem9N  38232  pexmidlem6N  38243  pl42lem1N  38247  istrnN  38425  djavalN  39403  dihmeetlem9N  39583  dihmeetlem11N  39585  dihmeetlem12N  39586  dihoml4  39645  djhval  39666  dochexmidlem6  39733  lclkrlem2b  39776  lcfrlem20  39830  lcfrlem23  39833  metakunt20  40401  elrfi  40778  isnacs  40788  mrefg2  40791  mapfzcons2  40803  coeq0i  40837  eldioph2lem2  40845  aomclem8  41149  kelac1  41151  islmodfg  41157  lnr2i  41204  fgraphopab  41298  ntrkbimka  41969  ntrk0kbimka  41970  isotone2  41980  ntrclskb  42000  ntrclsk3  42001  ntrclsk13  42002  neicvgbex  42043  disjrnmpt2  43053  disjinfi  43058  uzinico2  43436  uzinico3  43437  fsumiunss  43452  lptre2pt  43517  limsupresre  43573  limsuplesup  43576  limsupresico  43577  limsupvaluz  43585  limsuplt2  43630  liminfval  43636  limsupge  43638  liminfgval  43639  liminfval2  43645  liminfresico  43648  liminflelimsuplem  43652  liminflelimsup  43653  stoweidlem50  43927  stoweidlem57  43934  subsaliuncllem  44232  sge0val  44241  sge0iunmptlemre  44290  nnfoctbdjlem  44330  iundjiun  44335  vonvolmbllem  44535  smfpimcclem  44682  smfsuplem1  44686  f1cof1blem  44919  elbigo  46248  restclsseplem  46559  sepnsepo  46568  aacllem  46856