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

Theorem ineq1d 3846
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 3840 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cin 3606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614
This theorem is referenced by:  diftpsn3OLD  4365  iinrab2  4615  disji2  4668  disjprg  4680  disjxun  4683  riinint  5414  fnresdisj  6039  fnimadisj  6050  fninfp  6481  ecinxp  7865  fiint  8278  fival  8359  marypha1lem  8380  kmlem12  9021  fin23lem12  9191  fin23lem30  9202  fin23lem33  9205  ttukeylem1  9369  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwe2  9503  fzval2  12367  fvinim0ffz  12627  limsupval  14249  limsupgval  14251  ello1  14290  elo1  14301  fsum1p  14526  incexclem  14612  fprod1p  14742  smuval2  15251  smueqlem  15259  smumul  15262  setsdm  15939  isacs2  16361  acsfiel  16362  isacs1i  16365  catcval  16793  resscatc  16802  acsficl  17218  lsmdisj3  18142  lsmdisj3a  18148  dprdres  18473  dprdz  18475  dpjdisj  18498  lspdisj2  19175  indistopon  20853  restopnb  21027  ordtrest2  21056  isnrm  21187  cmpcov  21240  cmpsublem  21250  cmpsub  21251  tgcmp  21252  uncmp  21254  hauscmplem  21257  nconnsubb  21274  isnlly  21320  dissnlocfin  21380  kgeni  21388  kgencn3  21409  ptcld  21464  ptcnplem  21472  alexsublem  21895  alexsubb  21897  alexsubALTlem2  21899  alexsubALTlem4  21901  alexsubALT  21902  tmdgsum2  21947  tsmsval2  21980  ustexsym  22066  metrest  22376  qtopbaslem  22609  cnheibor  22801  bndth  22804  lebnumii  22812  iscph  23016  csscld  23094  clsocv  23095  ovolicc2  23336  voliunlem3  23366  ioombl  23379  uniioombllem2  23397  uniioombllem4  23400  uniioombllem6  23402  mbflimsup  23478  taylfval  24158  chtval  24881  ppival  24898  ppival2  24899  ppival2g  24900  chtfl  24920  ppiprm  24922  chtprm  24924  chtnprm  24925  chtdif  24929  ppidif  24934  prmorcht  24949  chdmj2  28517  cmcmlem  28578  pjoml2  28598  fh2  28606  mdbr  29281  mdi  29282  mdbr3  29284  mdbr4  29285  dmdmd  29287  dmdbr3  29292  dmdbr4  29293  dmdi4  29294  dmdbr5  29295  mddmd2  29296  mdsl1i  29308  cvmdi  29311  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd1lem3  29314  mdslmd1lem4  29315  mdslmd1i  29316  mdslmd3i  29319  csmdsymi  29321  mdexchi  29322  atomli  29369  atabsi  29388  sumdmdlem2  29406  dmdbr5ati  29409  difuncomp  29495  disji2f  29516  disjif2  29520  disjxpin  29527  disjunsn  29533  fnresin  29558  locfinreflem  30035  iscref  30039  ordtrest2NEW  30097  ordtconnlem1  30098  carsgclctunlem1  30507  totprobd  30616  probmeasb  30620  ballotlemfval  30679  ballotlemfp1  30681  ballotlemgun  30714  chtvalz  30835  bnj1385  31029  bnj1326  31220  iccllysconn  31358  mvrsval  31528  mrsubvrs  31545  mpstval  31558  msubvrs  31583  nosupbnd2lem1  31986  neibastop2lem  32480  neibastop2  32481  neibastop3  32482  limsucncmpi  32569  bj-ismoore  33184  ptrest  33538  mblfinlem2  33577  sstotbnd2  33703  cntotbnd  33725  heibor  33750  xrneq1  34279  l1cvat  34660  pmodlem2  35451  pmod2iN  35453  hlmod1i  35460  osumcllem3N  35562  osumcllem9N  35568  pexmidlem6N  35579  pl42lem1N  35583  istrnN  35762  djavalN  36741  dihmeetlem9N  36921  dihmeetlem11N  36923  dihmeetlem12N  36924  dihoml4  36983  djhval  37004  dochexmidlem6  37071  lclkrlem2b  37114  lcfrlem20  37168  lcfrlem23  37171  elrfi  37574  isnacs  37584  mrefg2  37587  mapfzcons2  37599  coeq0i  37633  eldioph2lem2  37641  aomclem8  37948  kelac1  37950  islmodfg  37956  lnr2i  38003  fgraphopab  38105  ntrkbimka  38653  ntrk0kbimka  38654  isotone2  38664  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  neicvgbex  38727  disjrnmpt2  39689  disjinfi  39694  uzinico2  40107  uzinico3  40108  fsumiunss  40125  lptre2pt  40190  limsupresre  40246  limsuplesup  40249  limsupresico  40250  limsupvaluz  40258  limsuplt2  40303  liminfval  40309  limsupge  40311  liminfgval  40312  liminfval2  40318  liminfresico  40321  liminflelimsuplem  40325  liminflelimsup  40326  stoweidlem50  40585  stoweidlem57  40592  subsaliuncllem  40893  sge0val  40901  sge0iunmptlemre  40950  nnfoctbdjlem  40990  iundjiun  40995  vonvolmbllem  41195  smfpimcclem  41334  smfsuplem1  41338  elbigo  42670  aacllem  42875
  Copyright terms: Public domain W3C validator