Theorem ineq1d 4159

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

Syntax hints:   → wi 4   = wceq 1542   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-in 3896

This theorem is referenced by:  iinrab2  5012  disji2  5069  disjprg  5081  disjxun  5083  riinint  5927  fnresdisj  6618  fnimadisj  6630  fninfp  7129  ecinxp  8739  fiint  9237  fival  9325  marypha1lem  9346  kmlem12  10084  fin23lem12  10253  fin23lem30  10264  fin23lem33  10267  ttukeylem1  10431  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2  10566  fzval2  13464  fvinim0ffz  13744  limsupval  15436  limsupgval  15438  ello1  15477  elo1  15488  fsum1p  15715  incexclem  15801  fprod1p  15933  smuval2  16451  smueqlem  16459  smumul  16462  setsdm  17140  isacs2  17619  acsfiel  17620  isacs1i  17623  cat1lem  18063  catcval  18067  resscatc  18076  acsficl  18513  lsmdisj3  19658  lsmdisj3a  19664  dprdres  20005  dprdz  20007  dpjdisj  20030  lspdisj2  21125  indistopon  22966  restopnb  23140  ordtrest2  23169  isnrm  23300  cmpcov  23354  cmpsublem  23364  cmpsub  23365  tgcmp  23366  uncmp  23368  hauscmplem  23371  nconnsubb  23388  isnlly  23434  dissnlocfin  23494  kgeni  23502  kgencn3  23523  ptcld  23578  ptcnplem  23586  alexsublem  24009  alexsubb  24011  alexsubALTlem2  24013  alexsubALTlem4  24015  alexsubALT  24016  tmdgsum2  24061  tsmsval2  24095  ustexsym  24181  metrest  24489  qtopbaslem  24723  cnheibor  24922  bndth  24925  lebnumii  24933  iscph  25137  csscld  25216  clsocv  25217  cphsscph  25218  ovolicc2  25489  voliunlem3  25519  ioombl  25532  uniioombllem2  25550  uniioombllem4  25553  uniioombllem6  25555  mbflimsup  25633  taylfval  26324  chtval  27073  ppival  27090  ppival2  27091  ppival2g  27092  chtfl  27112  ppiprm  27114  chtprm  27116  chtnprm  27117  chtdif  27121  ppidif  27126  prmorcht  27141  nosupbnd2lem1  27679  dfpth2  29797  chdmj2  31601  cmcmlem  31662  pjoml2  31682  fh2  31690  mdbr  32365  mdi  32366  mdbr3  32368  mdbr4  32369  dmdmd  32371  dmdbr3  32376  dmdbr4  32377  dmdi4  32378  dmdbr5  32379  mddmd2  32380  mdsl1i  32392  cvmdi  32395  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd1lem3  32398  mdslmd1lem4  32399  mdslmd1i  32400  mdslmd3i  32403  csmdsymi  32405  mdexchi  32406  atomli  32453  atabsi  32472  sumdmdlem2  32490  dmdbr5ati  32493  difuncomp  32623  disji2f  32647  disjif2  32651  disjxpin  32658  disjunsn  32664  fnresin  32697  cycpmco2f1  33185  cycpmconjslem2  33216  locfinreflem  33984  iscref  33988  ordtrest2NEW  34067  ordtconnlem1  34068  carsgclctunlem1  34461  totprobd  34570  probmeasb  34574  ballotlemfval  34634  ballotlemfp1  34636  ballotlemgun  34669  chtvalz  34773  bnj1385  34974  bnj1326  35168  vonf1owev  35290  iccllysconn  35432  satfv1  35545  mvrsval  35687  mrsubvrs  35704  mpstval  35717  msubvrs  35742  neibastop2lem  36542  neibastop2  36543  neibastop3  36544  limsucncmpi  36627  dfttc4  36712  mh-infprim2bi  36729  bj-ismoore  37417  fvineqsnf1  37726  pibt2  37733  ptrest  37940  mblfinlem2  37979  sstotbnd2  38095  cntotbnd  38117  heibor  38142  xrneq1  38717  disjressuc2  38732  ecqmap  38770  l1cvat  39501  pmodlem2  40293  pmod2iN  40295  hlmod1i  40302  osumcllem3N  40404  osumcllem9N  40410  pexmidlem6N  40421  pl42lem1N  40425  istrnN  40603  djavalN  41581  dihmeetlem9N  41761  dihmeetlem11N  41763  dihmeetlem12N  41764  dihoml4  41823  djhval  41844  dochexmidlem6  41911  lclkrlem2b  41954  lcfrlem20  42008  lcfrlem23  42011  elrfi  43126  isnacs  43136  mrefg2  43139  mapfzcons2  43151  coeq0i  43185  eldioph2lem2  43193  aomclem8  43489  kelac1  43491  islmodfg  43497  lnr2i  43544  fgraphopab  43631  ntrkbimka  44465  ntrk0kbimka  44466  isotone2  44476  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  neicvgbex  44539  disjrnmpt2  45618  disjinfi  45622  uzinico2  45991  uzinico3  45992  fsumiunss  46005  lptre2pt  46068  limsupresre  46124  limsuplesup  46127  limsupresico  46128  limsupvaluz  46136  limsuplt2  46181  liminfval  46187  limsupge  46189  liminfgval  46190  liminfval2  46196  liminfresico  46199  liminflelimsuplem  46203  liminflelimsup  46204  stoweidlem50  46478  stoweidlem57  46485  subsaliuncllem  46785  sge0val  46794  sge0iunmptlemre  46843  nnfoctbdjlem  46883  iundjiun  46888  vonvolmbllem  47088  smfpimcclem  47235  smfsuplem1  47239  f1cof1blem  47522  3f1oss1  47523  grimuhgr  48363  elbigo  49027  restclsseplem  49390  sepnsepo  49399  aacllem  50276