Theorem ineq1d 4199

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

Syntax hints:   → wi 4   = wceq 1539   ∩ cin 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-in 3938

This theorem is referenced by:  iinrab2  5050  disji2  5107  disjprg  5119  disjxun  5121  riinint  5962  fnresdisj  6668  fnimadisj  6680  fninfp  7176  ecinxp  8814  fiint  9348  fiintOLD  9349  fival  9434  marypha1lem  9455  kmlem12  10184  fin23lem12  10353  fin23lem30  10364  fin23lem33  10367  ttukeylem1  10531  fpwwe2cbv  10652  fpwwe2lem2  10654  fpwwe2  10665  fzval2  13532  fvinim0ffz  13807  limsupval  15492  limsupgval  15494  ello1  15533  elo1  15544  fsum1p  15771  incexclem  15854  fprod1p  15986  smuval2  16501  smueqlem  16509  smumul  16512  setsdm  17189  isacs2  17667  acsfiel  17668  isacs1i  17671  cat1lem  18112  catcval  18116  resscatc  18125  acsficl  18561  lsmdisj3  19669  lsmdisj3a  19675  dprdres  20016  dprdz  20018  dpjdisj  20041  lspdisj2  21097  indistopon  22955  restopnb  23129  ordtrest2  23158  isnrm  23289  cmpcov  23343  cmpsublem  23353  cmpsub  23354  tgcmp  23355  uncmp  23357  hauscmplem  23360  nconnsubb  23377  isnlly  23423  dissnlocfin  23483  kgeni  23491  kgencn3  23512  ptcld  23567  ptcnplem  23575  alexsublem  23998  alexsubb  24000  alexsubALTlem2  24002  alexsubALTlem4  24004  alexsubALT  24005  tmdgsum2  24050  tsmsval2  24084  ustexsym  24170  metrest  24481  qtopbaslem  24715  cnheibor  24923  bndth  24926  lebnumii  24934  iscph  25140  csscld  25219  clsocv  25220  cphsscph  25221  ovolicc2  25493  voliunlem3  25523  ioombl  25536  uniioombllem2  25554  uniioombllem4  25557  uniioombllem6  25559  mbflimsup  25637  taylfval  26336  chtval  27089  ppival  27106  ppival2  27107  ppival2g  27108  chtfl  27128  ppiprm  27130  chtprm  27132  chtnprm  27133  chtdif  27137  ppidif  27142  prmorcht  27157  nosupbnd2lem1  27696  dfpth2  29677  chdmj2  31477  cmcmlem  31538  pjoml2  31558  fh2  31566  mdbr  32241  mdi  32242  mdbr3  32244  mdbr4  32245  dmdmd  32247  dmdbr3  32252  dmdbr4  32253  dmdi4  32254  dmdbr5  32255  mddmd2  32256  mdsl1i  32268  cvmdi  32271  mdslmd1lem1  32272  mdslmd1lem2  32273  mdslmd1lem3  32274  mdslmd1lem4  32275  mdslmd1i  32276  mdslmd3i  32279  csmdsymi  32281  mdexchi  32282  atomli  32329  atabsi  32348  sumdmdlem2  32366  dmdbr5ati  32369  difuncomp  32501  disji2f  32525  disjif2  32529  disjxpin  32536  disjunsn  32542  fnresin  32571  cycpmco2f1  33083  cycpmconjslem2  33114  locfinreflem  33798  iscref  33802  ordtrest2NEW  33881  ordtconnlem1  33882  carsgclctunlem1  34278  totprobd  34387  probmeasb  34391  ballotlemfval  34451  ballotlemfp1  34453  ballotlemgun  34486  chtvalz  34603  bnj1385  34805  bnj1326  34999  iccllysconn  35214  satfv1  35327  mvrsval  35469  mrsubvrs  35486  mpstval  35499  msubvrs  35524  neibastop2lem  36320  neibastop2  36321  neibastop3  36322  limsucncmpi  36405  bj-ismoore  37065  fvineqsnf1  37370  pibt2  37377  ptrest  37585  mblfinlem2  37624  sstotbnd2  37740  cntotbnd  37762  heibor  37787  xrneq1  38337  disjressuc2  38348  l1cvat  39015  pmodlem2  39808  pmod2iN  39810  hlmod1i  39817  osumcllem3N  39919  osumcllem9N  39925  pexmidlem6N  39936  pl42lem1N  39940  istrnN  40118  djavalN  41096  dihmeetlem9N  41276  dihmeetlem11N  41278  dihmeetlem12N  41279  dihoml4  41338  djhval  41359  dochexmidlem6  41426  lclkrlem2b  41469  lcfrlem20  41523  lcfrlem23  41526  metakunt20  42184  elrfi  42668  isnacs  42678  mrefg2  42681  mapfzcons2  42693  coeq0i  42727  eldioph2lem2  42735  aomclem8  43036  kelac1  43038  islmodfg  43044  lnr2i  43091  fgraphopab  43178  ntrkbimka  44013  ntrk0kbimka  44014  isotone2  44024  ntrclskb  44044  ntrclsk3  44045  ntrclsk13  44046  neicvgbex  44087  disjrnmpt2  45150  disjinfi  45154  uzinico2  45532  uzinico3  45533  fsumiunss  45547  lptre2pt  45612  limsupresre  45668  limsuplesup  45671  limsupresico  45672  limsupvaluz  45680  limsuplt2  45725  liminfval  45731  limsupge  45733  liminfgval  45734  liminfval2  45740  liminfresico  45743  liminflelimsuplem  45747  liminflelimsup  45748  stoweidlem50  46022  stoweidlem57  46029  subsaliuncllem  46329  sge0val  46338  sge0iunmptlemre  46387  nnfoctbdjlem  46427  iundjiun  46432  vonvolmbllem  46632  smfpimcclem  46779  smfsuplem1  46783  f1cof1blem  47044  3f1oss1  47045  grimuhgr  47836  elbigo  48430  restclsseplem  48772  sepnsepo  48781  aacllem  49328