Theorem ineq1d 4211

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-in 3955

This theorem is referenced by:  iinrab2  5073  disji2  5130  disjprgw  5143  disjprg  5144  disjxun  5146  riinint  5967  fnresdisj  6670  fnimadisj  6682  fninfp  7174  ecinxp  8788  fiint  9326  fival  9409  marypha1lem  9430  kmlem12  10158  fin23lem12  10328  fin23lem30  10339  fin23lem33  10342  ttukeylem1  10506  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwe2  10640  fzval2  13491  fvinim0ffz  13755  limsupval  15422  limsupgval  15424  ello1  15463  elo1  15474  fsum1p  15703  incexclem  15786  fprod1p  15916  smuval2  16427  smueqlem  16435  smumul  16438  setsdm  17107  isacs2  17601  acsfiel  17602  isacs1i  17605  cat1lem  18050  catcval  18054  resscatc  18063  acsficl  18504  lsmdisj3  19592  lsmdisj3a  19598  dprdres  19939  dprdz  19941  dpjdisj  19964  lspdisj2  20885  indistopon  22724  restopnb  22899  ordtrest2  22928  isnrm  23059  cmpcov  23113  cmpsublem  23123  cmpsub  23124  tgcmp  23125  uncmp  23127  hauscmplem  23130  nconnsubb  23147  isnlly  23193  dissnlocfin  23253  kgeni  23261  kgencn3  23282  ptcld  23337  ptcnplem  23345  alexsublem  23768  alexsubb  23770  alexsubALTlem2  23772  alexsubALTlem4  23774  alexsubALT  23775  tmdgsum2  23820  tsmsval2  23854  ustexsym  23940  metrest  24253  qtopbaslem  24495  cnheibor  24695  bndth  24698  lebnumii  24706  iscph  24911  csscld  24990  clsocv  24991  cphsscph  24992  ovolicc2  25263  voliunlem3  25293  ioombl  25306  uniioombllem2  25324  uniioombllem4  25327  uniioombllem6  25329  mbflimsup  25407  taylfval  26095  chtval  26838  ppival  26855  ppival2  26856  ppival2g  26857  chtfl  26877  ppiprm  26879  chtprm  26881  chtnprm  26882  chtdif  26886  ppidif  26891  prmorcht  26906  nosupbnd2lem1  27442  chdmj2  31038  cmcmlem  31099  pjoml2  31119  fh2  31127  mdbr  31802  mdi  31803  mdbr3  31805  mdbr4  31806  dmdmd  31808  dmdbr3  31813  dmdbr4  31814  dmdi4  31815  dmdbr5  31816  mddmd2  31817  mdsl1i  31829  cvmdi  31832  mdslmd1lem1  31833  mdslmd1lem2  31834  mdslmd1lem3  31835  mdslmd1lem4  31836  mdslmd1i  31837  mdslmd3i  31840  csmdsymi  31842  mdexchi  31843  atomli  31890  atabsi  31909  sumdmdlem2  31927  dmdbr5ati  31930  difuncomp  32040  disji2f  32063  disjif2  32067  disjxpin  32074  disjunsn  32080  fnresin  32105  cycpmco2f1  32541  cycpmconjslem2  32572  locfinreflem  33106  iscref  33110  ordtrest2NEW  33189  ordtconnlem1  33190  carsgclctunlem1  33602  totprobd  33711  probmeasb  33715  ballotlemfval  33774  ballotlemfp1  33776  ballotlemgun  33809  chtvalz  33927  bnj1385  34129  bnj1326  34323  iccllysconn  34527  satfv1  34640  mvrsval  34782  mrsubvrs  34799  mpstval  34812  msubvrs  34837  neibastop2lem  35548  neibastop2  35549  neibastop3  35550  limsucncmpi  35633  bj-ismoore  36289  fvineqsnf1  36594  pibt2  36601  ptrest  36790  mblfinlem2  36829  sstotbnd2  36945  cntotbnd  36967  heibor  36992  xrneq1  37550  disjressuc2  37561  l1cvat  38228  pmodlem2  39021  pmod2iN  39023  hlmod1i  39030  osumcllem3N  39132  osumcllem9N  39138  pexmidlem6N  39149  pl42lem1N  39153  istrnN  39331  djavalN  40309  dihmeetlem9N  40489  dihmeetlem11N  40491  dihmeetlem12N  40492  dihoml4  40551  djhval  40572  dochexmidlem6  40639  lclkrlem2b  40682  lcfrlem20  40736  lcfrlem23  40739  metakunt20  41310  elrfi  41734  isnacs  41744  mrefg2  41747  mapfzcons2  41759  coeq0i  41793  eldioph2lem2  41801  aomclem8  42105  kelac1  42107  islmodfg  42113  lnr2i  42160  fgraphopab  42254  ntrkbimka  43091  ntrk0kbimka  43092  isotone2  43102  ntrclskb  43122  ntrclsk3  43123  ntrclsk13  43124  neicvgbex  43165  disjrnmpt2  44186  disjinfi  44190  uzinico2  44574  uzinico3  44575  fsumiunss  44590  lptre2pt  44655  limsupresre  44711  limsuplesup  44714  limsupresico  44715  limsupvaluz  44723  limsuplt2  44768  liminfval  44774  limsupge  44776  liminfgval  44777  liminfval2  44783  liminfresico  44786  liminflelimsuplem  44790  liminflelimsup  44791  stoweidlem50  45065  stoweidlem57  45072  subsaliuncllem  45372  sge0val  45381  sge0iunmptlemre  45430  nnfoctbdjlem  45470  iundjiun  45475  vonvolmbllem  45675  smfpimcclem  45822  smfsuplem1  45826  f1cof1blem  46083  elbigo  47325  restclsseplem  47635  sepnsepo  47644  aacllem  47936