MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq1d Structured version   Visualization version   GIF version

Theorem ineq1d 4170
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
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq1 4164 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  cin 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3407  df-in 3916
This theorem is referenced by:  iinrab2  5029  disji2  5086  disjprgw  5099  disjprg  5100  disjxun  5102  riinint  5920  fnresdisj  6617  fnimadisj  6629  fninfp  7115  ecinxp  8665  fiint  9202  fival  9282  marypha1lem  9303  kmlem12  10031  fin23lem12  10201  fin23lem30  10212  fin23lem33  10215  ttukeylem1  10379  fpwwe2cbv  10500  fpwwe2lem2  10502  fpwwe2  10513  fzval2  13356  fvinim0ffz  13620  limsupval  15291  limsupgval  15293  ello1  15332  elo1  15343  fsum1p  15573  incexclem  15656  fprod1p  15786  smuval2  16297  smueqlem  16305  smumul  16308  setsdm  16977  isacs2  17468  acsfiel  17469  isacs1i  17472  cat1lem  17917  catcval  17921  resscatc  17930  acsficl  18371  lsmdisj3  19394  lsmdisj3a  19400  dprdres  19736  dprdz  19738  dpjdisj  19761  lspdisj2  20511  indistopon  22273  restopnb  22448  ordtrest2  22477  isnrm  22608  cmpcov  22662  cmpsublem  22672  cmpsub  22673  tgcmp  22674  uncmp  22676  hauscmplem  22679  nconnsubb  22696  isnlly  22742  dissnlocfin  22802  kgeni  22810  kgencn3  22831  ptcld  22886  ptcnplem  22894  alexsublem  23317  alexsubb  23319  alexsubALTlem2  23321  alexsubALTlem4  23323  alexsubALT  23324  tmdgsum2  23369  tsmsval2  23403  ustexsym  23489  metrest  23802  qtopbaslem  24044  cnheibor  24240  bndth  24243  lebnumii  24251  iscph  24456  csscld  24535  clsocv  24536  cphsscph  24537  ovolicc2  24808  voliunlem3  24838  ioombl  24851  uniioombllem2  24869  uniioombllem4  24872  uniioombllem6  24874  mbflimsup  24952  taylfval  25640  chtval  26381  ppival  26398  ppival2  26399  ppival2g  26400  chtfl  26420  ppiprm  26422  chtprm  26424  chtnprm  26425  chtdif  26429  ppidif  26434  prmorcht  26449  nosupbnd2lem1  26985  chdmj2  30258  cmcmlem  30319  pjoml2  30339  fh2  30347  mdbr  31022  mdi  31023  mdbr3  31025  mdbr4  31026  dmdmd  31028  dmdbr3  31033  dmdbr4  31034  dmdi4  31035  dmdbr5  31036  mddmd2  31037  mdsl1i  31049  cvmdi  31052  mdslmd1lem1  31053  mdslmd1lem2  31054  mdslmd1lem3  31055  mdslmd1lem4  31056  mdslmd1i  31057  mdslmd3i  31060  csmdsymi  31062  mdexchi  31063  atomli  31110  atabsi  31129  sumdmdlem2  31147  dmdbr5ati  31150  difuncomp  31257  disji2f  31280  disjif2  31284  disjxpin  31291  disjunsn  31297  fnresin  31325  cycpmco2f1  31755  cycpmconjslem2  31786  locfinreflem  32182  iscref  32186  ordtrest2NEW  32265  ordtconnlem1  32266  carsgclctunlem1  32678  totprobd  32787  probmeasb  32791  ballotlemfval  32850  ballotlemfp1  32852  ballotlemgun  32885  chtvalz  33003  bnj1385  33205  bnj1326  33399  iccllysconn  33605  satfv1  33718  mvrsval  33860  mrsubvrs  33877  mpstval  33890  msubvrs  33915  neibastop2lem  34718  neibastop2  34719  neibastop3  34720  limsucncmpi  34803  bj-ismoore  35462  fvineqsnf1  35767  pibt2  35774  ptrest  35963  mblfinlem2  36002  sstotbnd2  36119  cntotbnd  36141  heibor  36166  xrneq1  36725  disjressuc2  36736  l1cvat  37403  pmodlem2  38196  pmod2iN  38198  hlmod1i  38205  osumcllem3N  38307  osumcllem9N  38313  pexmidlem6N  38324  pl42lem1N  38328  istrnN  38506  djavalN  39484  dihmeetlem9N  39664  dihmeetlem11N  39666  dihmeetlem12N  39667  dihoml4  39726  djhval  39747  dochexmidlem6  39814  lclkrlem2b  39857  lcfrlem20  39911  lcfrlem23  39914  metakunt20  40482  elrfi  40851  isnacs  40861  mrefg2  40864  mapfzcons2  40876  coeq0i  40910  eldioph2lem2  40918  aomclem8  41222  kelac1  41224  islmodfg  41230  lnr2i  41277  fgraphopab  41371  ntrkbimka  42043  ntrk0kbimka  42044  isotone2  42054  ntrclskb  42074  ntrclsk3  42075  ntrclsk13  42076  neicvgbex  42117  disjrnmpt2  43127  disjinfi  43132  uzinico2  43510  uzinico3  43511  fsumiunss  43526  lptre2pt  43591  limsupresre  43647  limsuplesup  43650  limsupresico  43651  limsupvaluz  43659  limsuplt2  43704  liminfval  43710  limsupge  43712  liminfgval  43713  liminfval2  43719  liminfresico  43722  liminflelimsuplem  43726  liminflelimsup  43727  stoweidlem50  44001  stoweidlem57  44008  subsaliuncllem  44306  sge0val  44315  sge0iunmptlemre  44364  nnfoctbdjlem  44404  iundjiun  44409  vonvolmbllem  44609  smfpimcclem  44756  smfsuplem1  44760  f1cof1blem  45008  elbigo  46337  restclsseplem  46647  sepnsepo  46656  aacllem  46944
  Copyright terms: Public domain W3C validator