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

Theorem sseq1 3974
Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 3964 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3956 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 483 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3956 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 482 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 211 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 216 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wss 3915
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  sseq12  3976  sseq1i  3977  sseq1d  3980  nssne2  4010  psseq1  4052  uneqdifeq  4455  sbss  4485  pwjust  4566  elpwg  4568  pwpw0  4778  sssn  4791  ssunsn2  4792  pwsnOLD  4863  unimax  4910  trss  5238  al0ssb  5270  sseliALT  5271  elssabg  5298  intabs  5304  vpwex  5337  nnullss  5424  exss  5425  friOLD  5599  releq  5737  iss  5994  relcnvtrg  6223  fununi  6581  ssimaex  6931  isofrlem  7290  onssmin  7732  tfis  7796  tfisi  7800  funcnvuni  7873  ffoss  7883  f1oweALT  7910  frxp  8063  frxp2  8081  frrlem1  8222  frrlem13  8234  wfrlem1OLD  8259  wfrlem4OLD  8263  wfrlem15OLD  8274  tfrlem1  8327  oawordeu  8507  coflton  8622  cofon1  8623  cofon2  8624  naddunif  8644  qsss  8724  boxcutc  8886  sbthlem2  9035  sbth  9044  findcard2d  9117  ssfi  9124  sbthfi  9153  php  9161  phpOLD  9173  isinf  9211  isinfOLD  9212  unbnn2  9251  domunfican  9271  fiint  9275  finsschain  9310  indexfi  9311  dffi3  9374  hartogslem1  9485  cantnfval2  9612  cantnfle  9614  cantnflem1  9632  tz9.1  9672  setind  9677  tcvalg  9681  frmin  9692  scott0  9829  bnd2  9836  carduni  9924  cardaleph  10032  alephinit  10038  aceq3lem  10063  dfac12lem3  10088  infmap2  10161  cflem  10189  cflm  10193  cflecard  10196  cfeq0  10199  cfsuc  10200  cfflb  10202  cfslb  10209  cfslb2n  10211  coftr  10216  fin23lem13  10275  fin23lem16  10278  fin23lem19  10279  fin23lem29  10284  fin1a2lem13  10355  itunitc  10364  domtriomlem  10385  axdc3lem2  10394  zorn2lem7  10445  zornn0g  10448  fpwwe2lem4  10577  pwfseqlem4a  10604  pwfseqlem4  10605  wunfi  10664  wunex2  10681  wuncval  10685  rankcf  10720  tskuni  10726  axgroth6  10771  axgroth3  10774  axgroth4  10775  fzoss1  13606  fsuppmapnn0fiubex  13904  hashf1lem2  14362  cleq1lem  14874  rtrclreclem4  14953  sumeq1  15580  fsumcvg3  15621  fsum2d  15663  fsumabs  15693  fsumrlim  15703  fsumo1  15704  fsumiun  15713  prodeq1f  15798  fprod2d  15871  lcmfunsnlem  16524  coprmprod  16544  vdwmc  16857  prmgaplem3  16932  prmgaplem4  16933  restsspw  17320  ismred2  17490  mrcval  17497  mrcuni  17508  acsfn  17546  isssc  17710  drsdirfi  18201  ipodrsima  18437  cntzssv  19115  pmtrfrn  19247  pmtrrn2  19249  pmtrdifellem1  19265  pmtrdifellem2  19266  sylow2alem2  19407  sylow2a  19408  efgval  19506  gsumzaddlem  19705  ablfac1eulem  19858  lspval  20452  lspindpi  20609  znf1o  20974  zntoslem  20979  aspval  21292  mplsubglem  21421  mpllsslem  21422  mplcoe1  21454  mplcoe5  21457  mdetunilem9  21985  uniopn  22262  fiinopn  22266  fiinbas  22318  baspartn  22320  eltg2  22324  eltg3  22328  topbas  22338  pptbas  22374  clsval  22404  neiint  22471  neips  22480  opnneissb  22481  opnssneib  22482  innei  22492  neiptoptop  22498  neiptopnei  22499  restbas  22525  restcld  22539  neitr  22547  restcls  22548  restntr  22549  cnpdis  22660  cmpsublem  22766  cmpsub  22767  fiuncmp  22771  unconn  22796  1stcfb  22812  2ndc1stc  22818  1stcrest  22820  2ndcctbss  22822  2ndcomap  22825  dis2ndc  22827  lly1stc  22863  refssex  22878  refun0  22882  llycmpkgen2  22917  txbas  22934  eltx  22935  ptuni2  22943  neitx  22974  ptpjopn  22979  ptcld  22980  txlm  23015  tx1stc  23017  txkgen  23019  xkopt  23022  xkococnlem  23026  ptcmpfi  23180  fbssfi  23204  opnfbas  23209  isfil2  23223  isfildlem  23224  snfil  23231  fsubbas  23234  ssfg  23239  fgss2  23241  fgcl  23245  fbasrn  23251  fgtr  23257  ufli  23281  uffix  23288  rnelfmlem  23319  fclscf  23392  alexsublem  23411  alexsubALTlem2  23415  alexsubALTlem3  23416  alexsubALTlem4  23417  alexsubALT  23418  tmdgsum2  23463  subgntr  23474  opnsubg  23475  qustgpopn  23487  tsmsfbas  23495  tsmsgsum  23506  tsmsres  23511  tsmsf1o  23512  tsmsxplem1  23520  tsmsxp  23522  isust  23571  ustssel  23573  ustincl  23575  ustdiag  23576  ustinvel  23577  ustexhalf  23578  ustexsym  23583  ust0  23587  restutop  23605  ustuqtop4  23612  utopsnneiplem  23615  blssexps  23795  blssex  23796  neibl  23873  blcld  23877  met1stc  23893  met2ndci  23894  metrest  23896  prdsxmslem2  23901  metustfbas  23929  cfilucfil  23931  metuel2  23937  metustbl  23938  restmetu  23942  dscopn  23945  isngp2  23969  tgioo  24175  tgqioo  24179  zdis  24195  xrge0tsms  24213  fsumcn  24249  volivth  24987  vitalilem2  24989  itgfsum  25207  limcun  25275  recnprss  25284  dvmptfsum  25355  ftc1a  25417  plyssc  25577  efopn  26029  jensen  26354  brsslt  27147  madef  27208  tglnunirn  27532  lpvtx  28061  umgredgprv  28100  usgredgprvALT  28185  issubgr2  28262  subgrprop2  28264  egrsubgr  28267  0uhgrsubgr  28269  frcond3  29255  hhsssh  30253  shintcl  30314  chintcl  30316  spanval  30317  omlsi  30388  pjoml  30420  chnlen0  30428  chsscon3  30484  chlejb1  30496  chnle  30498  spanun  30529  h1datom  30566  cmbr4i  30585  pjoml2  30595  pjoml3  30596  lecm  30601  osumcor2i  30628  osum  30629  spansncv  30637  pjcjt2  30676  pjopyth  30704  hstel2  31203  stj  31219  stcltr1i  31258  mdi  31279  mdbr3  31281  mdbr4  31282  dmdbr  31283  dmdmd  31284  dmdbr5  31292  mdsl1i  31305  mdslmd1lem3  31311  mdslmd1lem4  31312  mdslmd1i  31313  csmdsymi  31318  atss  31330  atom1d  31337  superpos  31338  chcv1  31339  shatomici  31342  shatomistici  31345  hatomistici  31346  chrelat2  31354  chirredi  31378  atcvat4i  31381  mdsymlem2  31388  mdsymlem6  31392  dmdbr6ati  31407  dmdbr7ati  31408  xrge0tsmsd  31941  gsumle  31974  gsumvsca1  32103  gsumvsca2  32104  prmidl  32252  ismxidl  32271  zarcls1  32490  zarclsun  32491  zarclsiin  32492  zarclsint  32493  zarclssn  32494  zartop  32497  zartopon  32498  zart0  32500  zarmxt1  32501  zarcmp  32503  rhmpreimacnlem  32505  rhmpreimacn  32506  tpr2rico  32533  issiga  32751  isrnsiga  32752  sigagenval  32779  measiuns  32856  dya2icoseg  32917  dya2iocnrect  32921  dya2iocuni  32923  carsgmon  32954  carsgsigalem  32955  carsgclctunlem2  32959  carsgclctun  32961  pmeasmono  32964  pmeasadd  32965  bnj517  33537  bnj1118  33636  bnj1145  33645  bnj1154  33651  bnj1452  33704  bnj1498  33713  fineqvpow  33737  fineqvac  33738  fineqvacALT  33739  pthhashvtx  33761  kur14lem1  33840  cvmopnlem  33912  dfon2lem3  34399  dfon2lem7  34403  brsset  34503  fness  34850  fneref  34851  fnessref  34858  neibastop2lem  34861  topmeet  34865  fnejoin2  34870  tailfb  34878  filnetlem4  34882  onsucsuccmpi  34944  bj-snglss  35470  bj-elpwgALT  35554  bj-restpw  35592  bj-imdirco  35690  dissneqlem  35840  relowlssretop  35863  relowlpssretop  35864  ctbssinf  35906  pibt2  35917  matunitlindflem1  36103  ptrecube  36107  poimirlem29  36136  mblfinlem2  36145  mblfinlem3  36146  mblfinlem4  36147  ismblfin  36148  ovoliunnfl  36149  voliunnfl  36151  volsupnfl  36152  indexa  36221  indexdom  36222  neificl  36241  istotbnd3  36259  sstotbnd2  36262  sstotbnd  36263  equivtotbnd  36266  ssbnd  36276  heiborlem1  36299  heiborlem6  36304  heiborlem8  36306  heiborlem10  36308  unichnidl  36519  pridl  36525  ismaxidl  36528  igenval  36549  igenval2  36554  ispridlc  36558  relcnveq3  36811  iss2  36834  elrelscnveq3  36982  brssr  36992  lsmsat  37499  lssatomic  37502  lssats  37503  lsat0cv  37524  lcvexchlem4  37528  lcvexchlem5  37529  lsatcvatlem  37540  l1cvpat  37545  ispsubsp  38237  linepsubN  38244  pclvalN  38382  ispsubclN  38429  ispsubcl2N  38439  pclfinclN  38442  diaelrnN  39537  docavalN  39615  dochval  39843  dvh4dimat  39930  dochexmidlem1  39952  lpolconN  39979  mapdordlem2  40129  ismrcd1  41050  ismrcd2  41051  ismrc  41053  mzpcompact2lem  41103  aomclem6  41415  hbtlem6  41485  rgspnval  41524  onintunirab  41590  rp-brsslt  41769  ssficl  41915  ssuncl  41916  ssdifcl  41917  sssymdifcl  41918  elmapintrab  41922  clcnvlem  41969  iunrelexpmin1  42054  iunrelexpmin2  42058  clsk3nimkb  42386  clsk1indlem1  42391  isotone1  42394  isotone2  42395  ntrclsiso  42413  gneispace  42480  gneispacess2  42492  onfrALTlem5  42898  onfrALTlem5VD  43241  islptre  43934  dvmptconst  44230  dvmptidg  44232  dvmulcncf  44240  dvdivcncf  44242  dvmptfprod  44260  stoweidlem51  44366  stoweidlem52  44367  fourierdlem103  44524  fourierdlem104  44525  ioorrnopnlem  44619  ioorrnopnxrlem  44621  salgenval  44636  ovnval2  44860  ovncvrrp  44879  ovnsubaddlem1  44885  ovnsubadd  44887  ovncvr2  44926  hspmbl  44944  elsetpreimafvssdm  45652  uspgrsprfo  46124  unilbss  46976  sepfsepc  47034  unilbeu  47084  ipolubdm  47086  ipoglbdm  47089  setrec1lem1  47206  setrec1lem4  47209  setrec2fun  47211  elsetrecslem  47218  elpglem2  47231
  Copyright terms: Public domain W3C validator