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

Theorem sseq1 3823
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 3813 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3805 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 469 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3805 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 468 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 203 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 208 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  sseq12  3825  sseq1i  3826  sseq1d  3829  nssne2  3859  psseq1  3892  uneqdifeq  4253  sbss  4277  pwjust  4352  elpw  4357  elpwg  4359  pwpw0  4534  sssn  4547  ssunsn2  4548  pwsnALT  4623  unimax  4667  trss  4955  al0ssb  4985  sseliALT  4986  elssabg  5011  intabs  5017  nnullss  5120  exss  5121  fri  5273  releq  5403  iss  5652  relcnvtr  5869  fununi  6175  ssimaex  6484  isofrlem  6814  onssmin  7227  tfis  7284  tfisi  7288  funcnvuni  7349  ffoss  7357  f1oweALT  7382  frxp  7521  wfrlem1  7649  wfrlem4  7653  wfrlem4OLD  7654  wfrlem15  7665  tfrlem1  7708  oawordeu  7872  qsss  8043  boxcutc  8188  sbthlem2  8310  sbth  8319  php  8383  isinf  8412  findcard2d  8441  unbnn2  8456  domunfican  8472  fiint  8476  finsschain  8512  indexfi  8513  dffi3  8576  hartogslem1  8686  cantnfval2  8813  cantnfle  8815  cantnflem1  8833  tz9.1  8852  setind  8857  tcvalg  8861  scott0  8996  bnd2  9003  carduni  9090  cardaleph  9195  alephinit  9201  aceq3lem  9226  dfac12lem3  9252  infmap2  9325  cflem  9353  cflm  9357  cflecard  9360  cfeq0  9363  cfsuc  9364  cfflb  9366  cfslb  9373  cfslb2n  9375  coftr  9380  fin23lem13  9439  fin23lem16  9442  fin23lem19  9443  fin23lem29  9448  fin1a2lem13  9519  itunitc  9528  domtriomlem  9549  axdc3lem2  9558  zorn2lem7  9609  zornn0g  9612  fpwwe2lem5  9741  pwfseqlem4a  9768  pwfseqlem4  9769  wunfi  9828  wunex2  9845  wuncval  9849  rankcf  9884  tskuni  9890  axgroth6  9935  axgroth3  9938  axgroth4  9939  fzoss1  12719  fsuppmapnn0fiubex  13015  hashf1lem2  13457  cleq1lem  13946  rtrclreclem4  14024  sumeq1  14642  fsumcvg3  14683  fsum2d  14725  fsumabs  14755  fsumrlim  14765  fsumo1  14766  fsumiun  14775  prodeq1f  14859  fprod2d  14932  lcmfunsnlem  15573  coprmprod  15593  vdwmc  15899  prmgaplem3  15974  prmgaplem4  15975  restsspw  16297  ismred2  16468  mrcval  16475  mrcuni  16486  acsfn  16524  isssc  16684  drsdirfi  17143  ipodrsima  17370  cntzssv  17962  pmtrfrn  18079  pmtrrn2  18081  pmtrdifellem1  18097  pmtrdifellem2  18098  isslw  18224  sylow2alem2  18234  sylow2a  18235  efgval  18331  gsumzaddlem  18522  ablfac1eulem  18673  lspval  19182  lspindpi  19340  aspval  19537  mplsubglem  19643  mpllsslem  19644  mplcoe1  19674  mplcoe5  19677  znf1o  20107  zntoslem  20112  mdetunilem9  20637  uniopn  20915  fiinopn  20919  fiinbas  20970  baspartn  20972  eltg2  20976  eltg3  20980  topbas  20990  pptbas  21026  clsval  21055  neival  21120  neiint  21122  neips  21131  opnneissb  21132  opnssneib  21133  innei  21143  neiptoptop  21149  neiptopnei  21150  restbas  21176  restcld  21190  neitr  21198  restcls  21199  restntr  21200  cnpdis  21311  cmpsublem  21416  cmpsub  21417  fiuncmp  21421  unconn  21446  1stcfb  21462  2ndc1stc  21468  1stcrest  21470  2ndcctbss  21472  2ndcomap  21475  dis2ndc  21477  lly1stc  21513  refssex  21528  refun0  21532  llycmpkgen2  21567  txbas  21584  eltx  21585  ptuni2  21593  neitx  21624  ptpjopn  21629  ptcld  21630  txlm  21665  tx1stc  21667  txkgen  21669  xkopt  21672  xkococnlem  21676  ptcmpfi  21830  fbssfi  21854  opnfbas  21859  isfil2  21873  isfildlem  21874  snfil  21881  fsubbas  21884  ssfg  21889  fgss2  21891  fgcl  21895  fbasrn  21901  fgtr  21907  ufli  21931  uffix  21938  rnelfmlem  21969  fclscf  22042  alexsublem  22061  alexsubALTlem2  22065  alexsubALTlem3  22066  alexsubALTlem4  22067  alexsubALT  22068  tmdgsum2  22113  subgntr  22123  opnsubg  22124  qustgpopn  22136  tsmsfbas  22144  tsmsgsum  22155  tsmsres  22160  tsmsf1o  22161  tsmsxplem1  22169  tsmsxp  22171  isust  22220  ustssel  22222  ustincl  22224  ustdiag  22225  ustinvel  22226  ustexhalf  22227  ustexsym  22232  ust0  22236  restutop  22254  ustuqtop4  22261  utopsnneiplem  22264  blssexps  22444  blssex  22445  neibl  22519  blcld  22523  met1stc  22539  met2ndci  22540  metrest  22542  prdsxmslem2  22547  metustfbas  22575  cfilucfil  22577  metuel2  22583  metustbl  22584  restmetu  22588  dscopn  22591  isngp2  22614  tgioo  22812  tgqioo  22816  zdis  22832  xrge0tsms  22850  fsumcn  22886  ovolval  23454  volivth  23588  vitalilem2  23590  itgfsum  23807  limcun  23873  recnprss  23882  dvmptfsum  23952  ftc1a  24014  plyssc  24170  efopn  24618  jensen  24929  tglnunirn  25657  lpvtx  26177  umgredgprv  26216  usgredgprvALT  26302  issubgr2  26380  subgrprop2  26382  egrsubgr  26385  0uhgrsubgr  26387  frcond3  27444  hhsssh  28454  shintcl  28517  chintcl  28519  spanval  28520  omlsi  28591  pjoml  28623  chnlen0  28631  chsscon3  28687  chlejb1  28699  chnle  28701  spanun  28732  h1datom  28769  cmbr4i  28788  pjoml2  28798  pjoml3  28799  lecm  28804  osumcor2i  28831  osum  28832  spansncv  28840  pjcjt2  28879  pjopyth  28907  hstel2  29406  stj  29422  stcltr1i  29461  mdi  29482  mdbr3  29484  mdbr4  29485  dmdbr  29486  dmdmd  29487  dmdbr5  29495  mdsl1i  29508  mdslmd1lem3  29514  mdslmd1lem4  29515  mdslmd1i  29516  csmdsymi  29521  atss  29533  atom1d  29540  superpos  29541  chcv1  29542  shatomici  29545  shatomistici  29548  hatomistici  29549  chrelat2  29557  chirredi  29581  atcvat4i  29584  mdsymlem2  29591  mdsymlem6  29595  dmdbr6ati  29610  dmdbr7ati  29611  gsumle  30104  gsumvsca1  30107  gsumvsca2  30108  xrge0tsmsd  30110  tpr2rico  30283  issiga  30499  isrnsigaOLD  30500  isrnsiga  30501  sigagenval  30528  measiuns  30605  dya2icoseg  30664  dya2iocnrect  30668  dya2iocuni  30670  carsgmon  30701  carsgsigalem  30702  carsgclctunlem2  30706  carsgclctun  30708  pmeasmono  30711  pmeasadd  30712  bnj517  31278  bnj1118  31375  bnj1145  31384  bnj1154  31390  bnj1452  31443  bnj1498  31452  kur14lem1  31511  cvmopnlem  31583  dfon2lem3  32010  dfon2lem7  32014  frmin  32063  frrlem1  32101  brsslt  32221  brsset  32317  fness  32665  fneref  32666  fnessref  32673  neibastop2lem  32676  topmeet  32680  fnejoin2  32685  tailfb  32693  filnetlem4  32697  onsucsuccmpi  32759  bj-snglss  33268  bj-restpw  33356  dissneqlem  33504  relowlssretop  33527  relowlpssretop  33528  matunitlindflem1  33718  ptrecube  33722  poimirlem29  33751  mblfinlem2  33760  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  indexa  33840  indexdom  33841  neificl  33860  istotbnd3  33881  sstotbnd2  33884  sstotbnd  33885  equivtotbnd  33888  ssbnd  33898  heiborlem1  33921  heiborlem6  33926  heiborlem8  33928  heiborlem10  33930  unichnidl  34141  pridl  34147  ismaxidl  34150  igenval  34171  igenval2  34176  ispridlc  34180  relcnveq3  34407  iss2  34425  elrelscnveq3  34554  brssr  34564  lsmsat  34788  lssatomic  34791  lssats  34792  lsat0cv  34813  lcvexchlem4  34817  lcvexchlem5  34818  lsatcvatlem  34829  l1cvpat  34834  ispsubsp  35525  linepsubN  35532  pclvalN  35670  ispsubclN  35717  ispsubcl2N  35727  pclfinclN  35730  diaelrnN  36826  docavalN  36904  dochval  37132  dvh4dimat  37219  dochexmidlem1  37241  lpolconN  37268  mapdordlem2  37418  ismrcd1  37763  ismrcd2  37764  ismrc  37766  mzpcompact2lem  37816  aomclem6  38130  hbtlem6  38200  rgspnval  38239  ssficl  38374  ssuncl  38375  ssdifcl  38376  sssymdifcl  38377  elmapintrab  38382  clcnvlem  38430  iunrelexpmin1  38500  iunrelexpmin2  38504  clsk3nimkb  38838  clsk1indlem1  38843  isotone1  38846  isotone2  38847  ntrclsiso  38865  gneispace  38932  gneispacess2  38944  onfrALTlem5  39255  onfrALTlem5VD  39615  islptre  40331  dvmptconst  40609  dvmptidg  40611  dvmulcncf  40620  dvdivcncf  40622  dvmptfprod  40640  stoweidlem51  40747  stoweidlem52  40748  fourierdlem103  40905  fourierdlem104  40906  ioorrnopnlem  41003  ioorrnopnxrlem  41005  salgenval  41020  ovnval2  41241  ovncvrrp  41260  ovnsubaddlem1  41266  ovnsubadd  41268  ovncvr2  41307  hspmbl  41325  uspgrsprfo  42324  setrec1lem1  43002  setrec1lem4  43005  setrec2fun  43007  elsetrecslem  43013  elpglem2  43026
  Copyright terms: Public domain W3C validator