Theorem ineq1d 4219

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-in 3958

This theorem is referenced by:  iinrab2  5070  disji2  5127  disjprg  5139  disjxun  5141  riinint  5982  fnresdisj  6688  fnimadisj  6700  fninfp  7194  ecinxp  8832  fiint  9366  fiintOLD  9367  fival  9452  marypha1lem  9473  kmlem12  10202  fin23lem12  10371  fin23lem30  10382  fin23lem33  10385  ttukeylem1  10549  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwe2  10683  fzval2  13550  fvinim0ffz  13825  limsupval  15510  limsupgval  15512  ello1  15551  elo1  15562  fsum1p  15789  incexclem  15872  fprod1p  16004  smuval2  16519  smueqlem  16527  smumul  16530  setsdm  17207  isacs2  17696  acsfiel  17697  isacs1i  17700  cat1lem  18141  catcval  18145  resscatc  18154  acsficl  18592  lsmdisj3  19701  lsmdisj3a  19707  dprdres  20048  dprdz  20050  dpjdisj  20073  lspdisj2  21129  indistopon  23008  restopnb  23183  ordtrest2  23212  isnrm  23343  cmpcov  23397  cmpsublem  23407  cmpsub  23408  tgcmp  23409  uncmp  23411  hauscmplem  23414  nconnsubb  23431  isnlly  23477  dissnlocfin  23537  kgeni  23545  kgencn3  23566  ptcld  23621  ptcnplem  23629  alexsublem  24052  alexsubb  24054  alexsubALTlem2  24056  alexsubALTlem4  24058  alexsubALT  24059  tmdgsum2  24104  tsmsval2  24138  ustexsym  24224  metrest  24537  qtopbaslem  24779  cnheibor  24987  bndth  24990  lebnumii  24998  iscph  25204  csscld  25283  clsocv  25284  cphsscph  25285  ovolicc2  25557  voliunlem3  25587  ioombl  25600  uniioombllem2  25618  uniioombllem4  25621  uniioombllem6  25623  mbflimsup  25701  taylfval  26400  chtval  27153  ppival  27170  ppival2  27171  ppival2g  27172  chtfl  27192  ppiprm  27194  chtprm  27196  chtnprm  27197  chtdif  27201  ppidif  27206  prmorcht  27221  nosupbnd2lem1  27760  dfpth2  29749  chdmj2  31549  cmcmlem  31610  pjoml2  31630  fh2  31638  mdbr  32313  mdi  32314  mdbr3  32316  mdbr4  32317  dmdmd  32319  dmdbr3  32324  dmdbr4  32325  dmdi4  32326  dmdbr5  32327  mddmd2  32328  mdsl1i  32340  cvmdi  32343  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd1lem3  32346  mdslmd1lem4  32347  mdslmd1i  32348  mdslmd3i  32351  csmdsymi  32353  mdexchi  32354  atomli  32401  atabsi  32420  sumdmdlem2  32438  dmdbr5ati  32441  difuncomp  32566  disji2f  32590  disjif2  32594  disjxpin  32601  disjunsn  32607  fnresin  32636  cycpmco2f1  33144  cycpmconjslem2  33175  locfinreflem  33839  iscref  33843  ordtrest2NEW  33922  ordtconnlem1  33923  carsgclctunlem1  34319  totprobd  34428  probmeasb  34432  ballotlemfval  34492  ballotlemfp1  34494  ballotlemgun  34527  chtvalz  34644  bnj1385  34846  bnj1326  35040  iccllysconn  35255  satfv1  35368  mvrsval  35510  mrsubvrs  35527  mpstval  35540  msubvrs  35565  neibastop2lem  36361  neibastop2  36362  neibastop3  36363  limsucncmpi  36446  bj-ismoore  37106  fvineqsnf1  37411  pibt2  37418  ptrest  37626  mblfinlem2  37665  sstotbnd2  37781  cntotbnd  37803  heibor  37828  xrneq1  38378  disjressuc2  38389  l1cvat  39056  pmodlem2  39849  pmod2iN  39851  hlmod1i  39858  osumcllem3N  39960  osumcllem9N  39966  pexmidlem6N  39977  pl42lem1N  39981  istrnN  40159  djavalN  41137  dihmeetlem9N  41317  dihmeetlem11N  41319  dihmeetlem12N  41320  dihoml4  41379  djhval  41400  dochexmidlem6  41467  lclkrlem2b  41510  lcfrlem20  41564  lcfrlem23  41567  metakunt20  42225  elrfi  42705  isnacs  42715  mrefg2  42718  mapfzcons2  42730  coeq0i  42764  eldioph2lem2  42772  aomclem8  43073  kelac1  43075  islmodfg  43081  lnr2i  43128  fgraphopab  43215  ntrkbimka  44051  ntrk0kbimka  44052  isotone2  44062  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  neicvgbex  44125  disjrnmpt2  45193  disjinfi  45197  uzinico2  45575  uzinico3  45576  fsumiunss  45590  lptre2pt  45655  limsupresre  45711  limsuplesup  45714  limsupresico  45715  limsupvaluz  45723  limsuplt2  45768  liminfval  45774  limsupge  45776  liminfgval  45777  liminfval2  45783  liminfresico  45786  liminflelimsuplem  45790  liminflelimsup  45791  stoweidlem50  46065  stoweidlem57  46072  subsaliuncllem  46372  sge0val  46381  sge0iunmptlemre  46430  nnfoctbdjlem  46470  iundjiun  46475  vonvolmbllem  46675  smfpimcclem  46822  smfsuplem1  46826  f1cof1blem  47086  3f1oss1  47087  grimuhgr  47878  elbigo  48472  restclsseplem  48812  sepnsepo  48821  aacllem  49320