Theorem ineq1d 4180

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

Syntax hints:   → wi 4   = wceq 1567   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-in 3920

This theorem is referenced by:  iinrab2  5035  disji2  5094  disjprg  5106  disjxun  5108  riinint  5960  fnresdisj  6653  fnimadisj  6665  fninfp  7170  ecinxp  8786  fiint  9282  fival  9368  marypha1lem  9389  kmlem12  10141  fin23lem12  10311  fin23lem30  10322  fin23lem33  10325  ttukeylem1  10489  fpwwe2cbv  10611  fpwwe2lem2  10613  fpwwe2  10624  fzval2  13534  fvinim0ffz  13814  limsupval  15521  limsupgval  15523  ello1  15562  elo1  15573  fsum1p  15800  incexclem  15886  fprod1p  16018  smuval2  16536  smueqlem  16544  smumul  16547  setsdm  17226  isacs2  17705  acsfiel  17706  isacs1i  17709  cat1lem  18149  catcval  18153  resscatc  18162  acsficl  18599  lsmdisj3  19749  lsmdisj3a  19755  dprdres  20096  dprdz  20098  dpjdisj  20121  lspdisj2  21225  indistopon  23123  restopnb  23297  ordtrest2  23326  isnrm  23457  cmpcov  23511  cmpsublem  23521  cmpsub  23522  tgcmp  23523  uncmp  23525  hauscmplem  23528  nconnsubb  23545  isnlly  23591  dissnlocfin  23651  kgeni  23659  kgencn3  23680  ptcld  23735  ptcnplem  23743  alexsublem  24166  alexsubb  24168  alexsubALTlem2  24170  alexsubALTlem4  24172  alexsubALT  24173  tmdgsum2  24218  tsmsval2  24252  ustexsym  24338  metrest  24646  qtopbaslem  24880  cnheibor  25079  bndth  25082  lebnumii  25090  iscph  25294  csscld  25373  clsocv  25374  cphsscph  25375  ovolicc2  25646  voliunlem3  25676  ioombl  25689  uniioombllem2  25707  uniioombllem4  25710  uniioombllem6  25712  mbflimsup  25790  taylfval  26484  chtval  27236  ppival  27253  ppival2  27254  ppival2g  27255  chtfl  27275  ppiprm  27277  chtprm  27279  chtnprm  27280  chtdif  27284  ppidif  27289  prmorcht  27304  nosupbnd2lem1  27841  dfpth2  30015  chdmj2  31819  cmcmlem  31880  pjoml2  31900  fh2  31908  mdbr  32583  mdi  32584  mdbr3  32586  mdbr4  32587  dmdmd  32589  dmdbr3  32594  dmdbr4  32595  dmdi4  32596  dmdbr5  32597  mddmd2  32598  mdsl1i  32610  cvmdi  32613  mdslmd1lem1  32614  mdslmd1lem2  32615  mdslmd1lem3  32616  mdslmd1lem4  32617  mdslmd1i  32618  mdslmd3i  32621  csmdsymi  32623  mdexchi  32624  atomli  32671  atabsi  32690  sumdmdlem2  32708  dmdbr5ati  32711  difuncomp  32835  disji2f  32859  disjif2  32863  disjxpin  32870  disjunsn  32876  fnresin  32906  cycpmco2f1  33381  cycpmconjslem2  33412  locfinreflem  34171  iscref  34175  ordtrest2NEW  34254  ordtconnlem1  34255  carsgclctunlem1  34648  totprobd  34757  probmeasb  34761  ballotlemfval  34821  ballotlemfp1  34823  ballotlemgun  34856  chtvalz  34957  bnj1385  35161  bnj1326  35355  vonf1wev  35487  vonf1owevOLD  35489  iccllysconn  35637  satfv1  35750  mvrsval  35892  mrsubvrs  35909  mpstval  35922  msubvrs  35947  neibastop2lem  36756  neibastop2  36757  neibastop3  36758  limsucncmpi  36841  dfttc4  36926  mh-infprim2bi  36943  bj-ismoore  37630  fvineqsnf1  37939  pibt2  37946  ptrest  38153  mblfinlem2  38192  sstotbnd2  38308  cntotbnd  38330  heibor  38355  xrneq1  38930  disjressuc2  38945  ecqmap  38983  l1cvat  39714  pmodlem2  40506  pmod2iN  40508  hlmod1i  40515  osumcllem3N  40617  osumcllem9N  40623  pexmidlem6N  40634  pl42lem1N  40638  istrnN  40816  djavalN  41794  dihmeetlem9N  41974  dihmeetlem11N  41976  dihmeetlem12N  41977  dihoml4  42036  djhval  42057  dochexmidlem6  42124  lclkrlem2b  42167  lcfrlem20  42221  lcfrlem23  42224  elrfi  43312  isnacs  43322  mrefg2  43325  mapfzcons2  43337  coeq0i  43371  eldioph2lem2  43379  aomclem8  43675  kelac1  43677  islmodfg  43683  lnr2i  43730  fgraphopab  43817  ntrkbimka  44651  ntrk0kbimka  44652  isotone2  44662  ntrclskb  44682  ntrclsk3  44683  ntrclsk13  44684  neicvgbex  44725  disjrnmpt2  45793  disjinfi  45797  uzinico2  46164  uzinico3  46165  fsumiunss  46178  lptre2pt  46241  limsupresre  46297  limsuplesup  46300  limsupresico  46301  limsupvaluz  46309  limsuplt2  46354  liminfval  46360  limsupge  46362  liminfgval  46363  liminfval2  46369  liminfresico  46372  liminflelimsuplem  46376  liminflelimsup  46377  stoweidlem50  46651  stoweidlem57  46658  subsaliuncllem  46958  sge0val  46967  sge0iunmptlemre  47016  nnfoctbdjlem  47056  iundjiun  47061  vonvolmbllem  47261  smfpimcclem  47408  smfsuplem1  47412  f1cof1blem  47695  3f1oss1  47696  grimuhgr  48536  elbigo  49211  restclsseplem  49573  sepnsepo  49582  aacllem  50470