Theorem ineq1d 4227

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

Syntax hints:   → wi 4   = wceq 1537   ∩ cin 3962

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-in 3970

This theorem is referenced by:  iinrab2  5075  disji2  5132  disjprg  5144  disjxun  5146  riinint  5985  fnresdisj  6689  fnimadisj  6701  fninfp  7194  ecinxp  8831  fiint  9364  fiintOLD  9365  fival  9450  marypha1lem  9471  kmlem12  10200  fin23lem12  10369  fin23lem30  10380  fin23lem33  10383  ttukeylem1  10547  fpwwe2cbv  10668  fpwwe2lem2  10670  fpwwe2  10681  fzval2  13547  fvinim0ffz  13822  limsupval  15507  limsupgval  15509  ello1  15548  elo1  15559  fsum1p  15786  incexclem  15869  fprod1p  16001  smuval2  16516  smueqlem  16524  smumul  16527  setsdm  17204  isacs2  17698  acsfiel  17699  isacs1i  17702  cat1lem  18150  catcval  18154  resscatc  18163  acsficl  18605  lsmdisj3  19716  lsmdisj3a  19722  dprdres  20063  dprdz  20065  dpjdisj  20088  lspdisj2  21147  indistopon  23024  restopnb  23199  ordtrest2  23228  isnrm  23359  cmpcov  23413  cmpsublem  23423  cmpsub  23424  tgcmp  23425  uncmp  23427  hauscmplem  23430  nconnsubb  23447  isnlly  23493  dissnlocfin  23553  kgeni  23561  kgencn3  23582  ptcld  23637  ptcnplem  23645  alexsublem  24068  alexsubb  24070  alexsubALTlem2  24072  alexsubALTlem4  24074  alexsubALT  24075  tmdgsum2  24120  tsmsval2  24154  ustexsym  24240  metrest  24553  qtopbaslem  24795  cnheibor  25001  bndth  25004  lebnumii  25012  iscph  25218  csscld  25297  clsocv  25298  cphsscph  25299  ovolicc2  25571  voliunlem3  25601  ioombl  25614  uniioombllem2  25632  uniioombllem4  25635  uniioombllem6  25637  mbflimsup  25715  taylfval  26415  chtval  27168  ppival  27185  ppival2  27186  ppival2g  27187  chtfl  27207  ppiprm  27209  chtprm  27211  chtnprm  27212  chtdif  27216  ppidif  27221  prmorcht  27236  nosupbnd2lem1  27775  chdmj2  31559  cmcmlem  31620  pjoml2  31640  fh2  31648  mdbr  32323  mdi  32324  mdbr3  32326  mdbr4  32327  dmdmd  32329  dmdbr3  32334  dmdbr4  32335  dmdi4  32336  dmdbr5  32337  mddmd2  32338  mdsl1i  32350  cvmdi  32353  mdslmd1lem1  32354  mdslmd1lem2  32355  mdslmd1lem3  32356  mdslmd1lem4  32357  mdslmd1i  32358  mdslmd3i  32361  csmdsymi  32363  mdexchi  32364  atomli  32411  atabsi  32430  sumdmdlem2  32448  dmdbr5ati  32451  difuncomp  32574  disji2f  32597  disjif2  32601  disjxpin  32608  disjunsn  32614  fnresin  32643  cycpmco2f1  33127  cycpmconjslem2  33158  locfinreflem  33801  iscref  33805  ordtrest2NEW  33884  ordtconnlem1  33885  carsgclctunlem1  34299  totprobd  34408  probmeasb  34412  ballotlemfval  34471  ballotlemfp1  34473  ballotlemgun  34506  chtvalz  34623  bnj1385  34825  bnj1326  35019  iccllysconn  35235  satfv1  35348  mvrsval  35490  mrsubvrs  35507  mpstval  35520  msubvrs  35545  neibastop2lem  36343  neibastop2  36344  neibastop3  36345  limsucncmpi  36428  bj-ismoore  37088  fvineqsnf1  37393  pibt2  37400  ptrest  37606  mblfinlem2  37645  sstotbnd2  37761  cntotbnd  37783  heibor  37808  xrneq1  38359  disjressuc2  38370  l1cvat  39037  pmodlem2  39830  pmod2iN  39832  hlmod1i  39839  osumcllem3N  39941  osumcllem9N  39947  pexmidlem6N  39958  pl42lem1N  39962  istrnN  40140  djavalN  41118  dihmeetlem9N  41298  dihmeetlem11N  41300  dihmeetlem12N  41301  dihoml4  41360  djhval  41381  dochexmidlem6  41448  lclkrlem2b  41491  lcfrlem20  41545  lcfrlem23  41548  metakunt20  42206  elrfi  42682  isnacs  42692  mrefg2  42695  mapfzcons2  42707  coeq0i  42741  eldioph2lem2  42749  aomclem8  43050  kelac1  43052  islmodfg  43058  lnr2i  43105  fgraphopab  43192  ntrkbimka  44028  ntrk0kbimka  44029  isotone2  44039  ntrclskb  44059  ntrclsk3  44060  ntrclsk13  44061  neicvgbex  44102  disjrnmpt2  45131  disjinfi  45135  uzinico2  45515  uzinico3  45516  fsumiunss  45531  lptre2pt  45596  limsupresre  45652  limsuplesup  45655  limsupresico  45656  limsupvaluz  45664  limsuplt2  45709  liminfval  45715  limsupge  45717  liminfgval  45718  liminfval2  45724  liminfresico  45727  liminflelimsuplem  45731  liminflelimsup  45732  stoweidlem50  46006  stoweidlem57  46013  subsaliuncllem  46313  sge0val  46322  sge0iunmptlemre  46371  nnfoctbdjlem  46411  iundjiun  46416  vonvolmbllem  46616  smfpimcclem  46763  smfsuplem1  46767  f1cof1blem  47024  3f1oss1  47025  grimuhgr  47816  elbigo  48401  restclsseplem  48711  sepnsepo  48720  aacllem  49032