Theorem ineq1d 4164

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

Syntax hints:   → wi 4   = wceq 1541   ∩ cin 3896

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-in 3904

This theorem is referenced by:  iinrab2  5013  disji2  5070  disjprg  5082  disjxun  5084  riinint  5906  fnresdisj  6596  fnimadisj  6608  fninfp  7103  ecinxp  8711  fiint  9206  fival  9291  marypha1lem  9312  kmlem12  10048  fin23lem12  10217  fin23lem30  10228  fin23lem33  10231  ttukeylem1  10395  fpwwe2cbv  10516  fpwwe2lem2  10518  fpwwe2  10529  fzval2  13405  fvinim0ffz  13684  limsupval  15376  limsupgval  15378  ello1  15417  elo1  15428  fsum1p  15655  incexclem  15738  fprod1p  15870  smuval2  16388  smueqlem  16396  smumul  16399  setsdm  17076  isacs2  17554  acsfiel  17555  isacs1i  17558  cat1lem  17998  catcval  18002  resscatc  18011  acsficl  18448  lsmdisj3  19590  lsmdisj3a  19596  dprdres  19937  dprdz  19939  dpjdisj  19962  lspdisj2  21059  indistopon  22911  restopnb  23085  ordtrest2  23114  isnrm  23245  cmpcov  23299  cmpsublem  23309  cmpsub  23310  tgcmp  23311  uncmp  23313  hauscmplem  23316  nconnsubb  23333  isnlly  23379  dissnlocfin  23439  kgeni  23447  kgencn3  23468  ptcld  23523  ptcnplem  23531  alexsublem  23954  alexsubb  23956  alexsubALTlem2  23958  alexsubALTlem4  23960  alexsubALT  23961  tmdgsum2  24006  tsmsval2  24040  ustexsym  24126  metrest  24434  qtopbaslem  24668  cnheibor  24876  bndth  24879  lebnumii  24887  iscph  25092  csscld  25171  clsocv  25172  cphsscph  25173  ovolicc2  25445  voliunlem3  25475  ioombl  25488  uniioombllem2  25506  uniioombllem4  25509  uniioombllem6  25511  mbflimsup  25589  taylfval  26288  chtval  27042  ppival  27059  ppival2  27060  ppival2g  27061  chtfl  27081  ppiprm  27083  chtprm  27085  chtnprm  27086  chtdif  27090  ppidif  27095  prmorcht  27110  nosupbnd2lem1  27649  dfpth2  29702  chdmj2  31502  cmcmlem  31563  pjoml2  31583  fh2  31591  mdbr  32266  mdi  32267  mdbr3  32269  mdbr4  32270  dmdmd  32272  dmdbr3  32277  dmdbr4  32278  dmdi4  32279  dmdbr5  32280  mddmd2  32281  mdsl1i  32293  cvmdi  32296  mdslmd1lem1  32297  mdslmd1lem2  32298  mdslmd1lem3  32299  mdslmd1lem4  32300  mdslmd1i  32301  mdslmd3i  32304  csmdsymi  32306  mdexchi  32307  atomli  32354  atabsi  32373  sumdmdlem2  32391  dmdbr5ati  32394  difuncomp  32525  disji2f  32549  disjif2  32553  disjxpin  32560  disjunsn  32566  fnresin  32599  cycpmco2f1  33085  cycpmconjslem2  33116  locfinreflem  33845  iscref  33849  ordtrest2NEW  33928  ordtconnlem1  33929  carsgclctunlem1  34322  totprobd  34431  probmeasb  34435  ballotlemfval  34495  ballotlemfp1  34497  ballotlemgun  34530  chtvalz  34634  bnj1385  34836  bnj1326  35030  vonf1owev  35144  iccllysconn  35286  satfv1  35399  mvrsval  35541  mrsubvrs  35558  mpstval  35571  msubvrs  35596  neibastop2lem  36394  neibastop2  36395  neibastop3  36396  limsucncmpi  36479  bj-ismoore  37139  fvineqsnf1  37444  pibt2  37451  ptrest  37659  mblfinlem2  37698  sstotbnd2  37814  cntotbnd  37836  heibor  37861  xrneq1  38409  disjressuc2  38420  l1cvat  39094  pmodlem2  39886  pmod2iN  39888  hlmod1i  39895  osumcllem3N  39997  osumcllem9N  40003  pexmidlem6N  40014  pl42lem1N  40018  istrnN  40196  djavalN  41174  dihmeetlem9N  41354  dihmeetlem11N  41356  dihmeetlem12N  41357  dihoml4  41416  djhval  41437  dochexmidlem6  41504  lclkrlem2b  41547  lcfrlem20  41601  lcfrlem23  41604  elrfi  42727  isnacs  42737  mrefg2  42740  mapfzcons2  42752  coeq0i  42786  eldioph2lem2  42794  aomclem8  43094  kelac1  43096  islmodfg  43102  lnr2i  43149  fgraphopab  43236  ntrkbimka  44071  ntrk0kbimka  44072  isotone2  44082  ntrclskb  44102  ntrclsk3  44103  ntrclsk13  44104  neicvgbex  44145  disjrnmpt2  45225  disjinfi  45229  uzinico2  45601  uzinico3  45602  fsumiunss  45615  lptre2pt  45678  limsupresre  45734  limsuplesup  45737  limsupresico  45738  limsupvaluz  45746  limsuplt2  45791  liminfval  45797  limsupge  45799  liminfgval  45800  liminfval2  45806  liminfresico  45809  liminflelimsuplem  45813  liminflelimsup  45814  stoweidlem50  46088  stoweidlem57  46095  subsaliuncllem  46395  sge0val  46404  sge0iunmptlemre  46453  nnfoctbdjlem  46493  iundjiun  46498  vonvolmbllem  46698  smfpimcclem  46845  smfsuplem1  46849  f1cof1blem  47105  3f1oss1  47106  grimuhgr  47918  elbigo  48583  restclsseplem  48946  sepnsepo  48955  aacllem  49833