Theorem ineq1d 4187

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

Syntax hints:   → wi 4   = wceq 1533   ∩ cin 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147  df-in 3942

This theorem is referenced by:  iinrab2  4984  disji2  5040  disjprgw  5053  disjprg  5054  disjxun  5056  riinint  5833  fnresdisj  6461  fnimadisj  6474  fninfp  6930  ecinxp  8366  fiint  8789  fival  8870  marypha1lem  8891  kmlem12  9581  fin23lem12  9747  fin23lem30  9758  fin23lem33  9761  ttukeylem1  9925  fpwwe2cbv  10046  fpwwe2lem2  10048  fpwwe2  10059  fzval2  12889  fvinim0ffz  13150  limsupval  14825  limsupgval  14827  ello1  14866  elo1  14877  fsum1p  15102  incexclem  15185  fprod1p  15316  smuval2  15825  smueqlem  15833  smumul  15836  setsdm  16511  isacs2  16918  acsfiel  16919  isacs1i  16922  catcval  17350  resscatc  17359  acsficl  17775  lsmdisj3  18803  lsmdisj3a  18809  dprdres  19144  dprdz  19146  dpjdisj  19169  lspdisj2  19893  indistopon  21603  restopnb  21777  ordtrest2  21806  isnrm  21937  cmpcov  21991  cmpsublem  22001  cmpsub  22002  tgcmp  22003  uncmp  22005  hauscmplem  22008  nconnsubb  22025  isnlly  22071  dissnlocfin  22131  kgeni  22139  kgencn3  22160  ptcld  22215  ptcnplem  22223  alexsublem  22646  alexsubb  22648  alexsubALTlem2  22650  alexsubALTlem4  22652  alexsubALT  22653  tmdgsum2  22698  tsmsval2  22732  ustexsym  22818  metrest  23128  qtopbaslem  23361  cnheibor  23553  bndth  23556  lebnumii  23564  iscph  23768  csscld  23846  clsocv  23847  cphsscph  23848  ovolicc2  24117  voliunlem3  24147  ioombl  24160  uniioombllem2  24178  uniioombllem4  24181  uniioombllem6  24183  mbflimsup  24261  taylfval  24941  chtval  25681  ppival  25698  ppival2  25699  ppival2g  25700  chtfl  25720  ppiprm  25722  chtprm  25724  chtnprm  25725  chtdif  25729  ppidif  25734  prmorcht  25749  chdmj2  29301  cmcmlem  29362  pjoml2  29382  fh2  29390  mdbr  30065  mdi  30066  mdbr3  30068  mdbr4  30069  dmdmd  30071  dmdbr3  30076  dmdbr4  30077  dmdi4  30078  dmdbr5  30079  mddmd2  30080  mdsl1i  30092  cvmdi  30095  mdslmd1lem1  30096  mdslmd1lem2  30097  mdslmd1lem3  30098  mdslmd1lem4  30099  mdslmd1i  30100  mdslmd3i  30103  csmdsymi  30105  mdexchi  30106  atomli  30153  atabsi  30172  sumdmdlem2  30190  dmdbr5ati  30193  difuncomp  30299  disji2f  30321  disjif2  30325  disjxpin  30332  disjunsn  30338  fnresin  30365  cycpmco2f1  30761  cycpmconjslem2  30792  locfinreflem  31099  iscref  31103  ordtrest2NEW  31161  ordtconnlem1  31162  carsgclctunlem1  31570  totprobd  31679  probmeasb  31683  ballotlemfval  31742  ballotlemfp1  31744  ballotlemgun  31777  chtvalz  31895  bnj1385  32099  bnj1326  32293  iccllysconn  32492  satfv1  32605  mvrsval  32747  mrsubvrs  32764  mpstval  32777  msubvrs  32802  nosupbnd2lem1  33210  neibastop2lem  33703  neibastop2  33704  neibastop3  33705  limsucncmpi  33788  bj-ismoore  34391  fvineqsnf1  34685  pibt2  34692  ptrest  34885  mblfinlem2  34924  sstotbnd2  35046  cntotbnd  35068  heibor  35093  xrneq1  35623  l1cvat  36185  pmodlem2  36977  pmod2iN  36979  hlmod1i  36986  osumcllem3N  37088  osumcllem9N  37094  pexmidlem6N  37105  pl42lem1N  37109  istrnN  37287  djavalN  38265  dihmeetlem9N  38445  dihmeetlem11N  38447  dihmeetlem12N  38448  dihoml4  38507  djhval  38528  dochexmidlem6  38595  lclkrlem2b  38638  lcfrlem20  38692  lcfrlem23  38695  elrfi  39284  isnacs  39294  mrefg2  39297  mapfzcons2  39309  coeq0i  39343  eldioph2lem2  39351  aomclem8  39654  kelac1  39656  islmodfg  39662  lnr2i  39709  fgraphopab  39803  ntrkbimka  40381  ntrk0kbimka  40382  isotone2  40392  ntrclskb  40412  ntrclsk3  40413  ntrclsk13  40414  neicvgbex  40455  disjrnmpt2  41442  disjinfi  41447  uzinico2  41831  uzinico3  41832  fsumiunss  41849  lptre2pt  41914  limsupresre  41970  limsuplesup  41973  limsupresico  41974  limsupvaluz  41982  limsuplt2  42027  liminfval  42033  limsupge  42035  liminfgval  42036  liminfval2  42042  liminfresico  42045  liminflelimsuplem  42049  liminflelimsup  42050  stoweidlem50  42329  stoweidlem57  42336  subsaliuncllem  42634  sge0val  42642  sge0iunmptlemre  42691  nnfoctbdjlem  42731  iundjiun  42736  vonvolmbllem  42936  smfpimcclem  43075  smfsuplem1  43079  elbigo  44605  aacllem  44896