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

Theorem sseq1 3588
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 3582 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3574 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 480 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3574 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 479 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 200 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 205 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sseq12  3590  sseq1i  3591  sseq1d  3594  nssne2  3624  psseq1  3655  uneqdifeq  4008  uneqdifeqOLD  4009  sbss  4033  pwjust  4108  elpw  4113  elpwg  4115  pwpw0  4283  sssn  4295  ssunsn2  4296  pwsnALT  4361  unimax  4403  trss  4683  trssOLD  4684  sseliALT  4713  elssabg  4740  intabs  4746  nnullss  4850  exss  4851  fri  4989  releq  5113  iss  5353  relcnvtr  5557  fununi  5863  ssimaex  6157  isofrlem  6467  onssmin  6866  tfis  6923  tfisi  6927  funcnvuni  6989  ffoss  6997  f1oweALT  7020  frxp  7151  wfrlem1  7278  wfrlem4  7282  wfrlem15  7293  tfrlem1  7336  oawordeu  7499  qsss  7672  boxcutc  7814  sbthlem2  7933  sbth  7942  php  8006  isinf  8035  findcard2d  8064  unbnn2  8079  domunfican  8095  fiint  8099  finsschain  8133  indexfi  8134  dffi3  8197  hartogslem1  8307  cantnfval2  8426  cantnfle  8428  cantnflem1  8446  tz9.1  8465  setind  8470  tcvalg  8474  scott0  8609  bnd2  8616  carduni  8667  cardaleph  8772  alephinit  8778  aceq3lem  8803  dfac12lem3  8827  infmap2  8900  cflem  8928  cflm  8932  cflecard  8935  cfeq0  8938  cfsuc  8939  cfflb  8941  cfslb  8948  cfslb2n  8950  coftr  8955  fin23lem13  9014  fin23lem16  9017  fin23lem19  9018  fin23lem29  9023  fin1a2lem13  9094  itunitc  9103  domtriomlem  9124  axdc3lem2  9133  zorn2lem7  9184  zornn0g  9187  fpwwe2lem5  9312  pwfseqlem4a  9339  pwfseqlem4  9340  wunfi  9399  wunex2  9416  wuncval  9420  rankcf  9455  tskuni  9461  axgroth6  9506  axgroth3  9509  axgroth4  9510  fzoss1  12321  fsuppmapnn0fiubex  12611  hashf1lem2  13051  cleq1lem  13517  rtrclreclem4  13597  sumeq1  14215  fsumcvg3  14255  fsum2d  14292  fsumabs  14322  fsumrlim  14332  fsumo1  14333  fsumiun  14342  prodeq1f  14425  fprod2d  14498  lcmfunsnlem  15140  coprmprod  15161  vdwmc  15468  prmgaplem3  15543  prmgaplem4  15544  restsspw  15863  ismred2  16034  mrcval  16041  mrcuni  16052  acsfn  16091  isssc  16251  drsdirfi  16709  ipodrsima  16936  cntzssv  17532  pmtrfrn  17649  pmtrrn2  17651  pmtrdifellem1  17667  pmtrdifellem2  17668  isslw  17794  sylow2alem2  17804  sylow2a  17805  efgval  17901  gsumzaddlem  18092  ablfac1eulem  18242  lspval  18744  lspindpi  18901  aspval  19097  mplsubglem  19203  mpllsslem  19204  mplcoe1  19234  mplcoe5  19237  znf1o  19666  zntoslem  19671  mdetunilem9  20192  uniopn  20474  fiinopn  20478  fiinbas  20514  baspartn  20516  eltg2  20520  eltg3  20524  topbas  20534  pptbas  20569  clsval  20598  neival  20663  neiint  20665  neips  20674  opnneissb  20675  opnssneib  20676  innei  20686  neiptoptop  20692  neiptopnei  20693  restbas  20719  restcld  20733  neitr  20741  restcls  20742  restntr  20743  cnpdis  20854  nrmsep3  20916  cmpsublem  20959  cmpsub  20960  fiuncmp  20964  uncon  20989  1stcfb  21005  2ndc1stc  21011  1stcrest  21013  2ndcctbss  21015  2ndcomap  21018  dis2ndc  21020  lly1stc  21056  refssex  21071  refun0  21075  llycmpkgen2  21110  txbas  21127  eltx  21128  ptuni2  21136  neitx  21167  ptpjopn  21172  ptcld  21173  txlm  21208  tx1stc  21210  txkgen  21212  xkopt  21215  xkococnlem  21219  ptcmpfi  21373  fbssfi  21398  opnfbas  21403  isfil2  21417  isfildlem  21418  snfil  21425  fsubbas  21428  ssfg  21433  fgss2  21435  fgcl  21439  fbasrn  21445  fgtr  21451  ufli  21475  uffix  21482  rnelfmlem  21513  fclscf  21586  alexsublem  21605  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALTlem4  21611  alexsubALT  21612  tmdgsum2  21657  subgntr  21667  opnsubg  21668  qustgpopn  21680  tsmsfbas  21688  tsmsgsum  21699  tsmsres  21704  tsmsf1o  21705  tsmsxplem1  21713  tsmsxp  21715  isust  21764  ustssel  21766  ustincl  21768  ustdiag  21769  ustinvel  21770  ustexhalf  21771  ustexsym  21776  ust0  21780  restutop  21798  ustuqtop4  21805  utopsnneiplem  21808  blssexps  21988  blssex  21989  neibl  22063  blcld  22067  met1stc  22083  met2ndci  22084  metrest  22086  prdsxmslem2  22091  metustfbas  22119  cfilucfil  22121  metuel2  22127  metustbl  22128  restmetu  22132  dscopn  22135  isngp2  22158  tgioo  22354  tgqioo  22358  zdis  22374  xrge0tsms  22392  fsumcn  22428  ovolval  22993  volivth  23125  vitalilem2  23128  itgfsum  23343  limcun  23409  recnprss  23418  dvmptfsum  23486  ftc1a  23548  plyssc  23704  efopn  24148  jensen  24459  tglnunirn  25188  usgraedgprv  25698  frisusgranb  26317  hhsssh  27303  shintcl  27366  chintcl  27368  spanval  27369  omlsi  27440  pjoml  27472  chnlen0  27480  chsscon3  27536  chlejb1  27548  chnle  27550  spanun  27581  h1datom  27618  cmbr4i  27637  pjoml2  27647  pjoml3  27648  lecm  27653  osumcor2i  27680  osum  27681  spansncv  27689  pjcjt2  27728  pjopyth  27756  hstel2  28255  stj  28271  stcltr1i  28310  mdi  28331  mdbr3  28333  mdbr4  28334  dmdbr  28335  dmdmd  28336  dmdbr5  28344  mdsl1i  28357  mdslmd1lem3  28363  mdslmd1lem4  28364  mdslmd1i  28365  csmdsymi  28370  atss  28382  atom1d  28389  superpos  28390  chcv1  28391  shatomici  28394  shatomistici  28397  hatomistici  28398  chrelat2  28406  chirredi  28430  atcvat4i  28433  mdsymlem2  28440  mdsymlem6  28444  dmdbr6ati  28459  dmdbr7ati  28460  gsumle  28903  gsumvsca1  28906  gsumvsca2  28907  xrge0tsmsd  28909  tpr2rico  29079  issiga  29294  isrnsigaOLD  29295  isrnsiga  29296  sigagenval  29323  measiuns  29400  dya2icoseg  29459  dya2iocnrect  29463  dya2iocuni  29465  carsgmon  29496  carsgsigalem  29497  carsgclctunlem2  29501  carsgclctun  29503  pmeasmono  29506  pmeasadd  29507  bnj517  30002  bnj1118  30099  bnj1145  30108  bnj1154  30114  bnj1452  30167  bnj1498  30176  kur14lem1  30235  cvmopnlem  30307  dfon2lem3  30727  dfon2lem7  30731  frmin  30776  frrlem1  30817  frrlem3  30819  brsset  30959  fness  31307  fneref  31308  fnessref  31315  neibastop2lem  31318  topmeet  31322  fnejoin2  31327  tailfb  31335  filnetlem4  31339  onsucsuccmpi  31405  bj-snglss  31934  bj-restpw  32009  dissneqlem  32146  relowlssretop  32170  relowlpssretop  32171  matunitlindflem1  32358  ptrecube  32362  poimirlem29  32391  mblfinlem2  32400  mblfinlem3  32401  mblfinlem4  32402  ismblfin  32403  ovoliunnfl  32404  voliunnfl  32406  volsupnfl  32407  indexa  32481  indexdom  32482  neificl  32502  istotbnd3  32523  sstotbnd2  32526  sstotbnd  32527  equivtotbnd  32530  ssbnd  32540  heiborlem1  32563  heiborlem6  32568  heiborlem8  32570  heiborlem10  32572  unichnidl  32783  pridl  32789  ismaxidl  32792  igenval  32813  igenval2  32818  ispridlc  32822  lsmsat  33096  lssatomic  33099  lssats  33100  lsat0cv  33121  lcvexchlem4  33125  lcvexchlem5  33126  lsatcvatlem  33137  l1cvpat  33142  ispsubsp  33832  linepsubN  33839  pclvalN  33977  ispsubclN  34024  ispsubcl2N  34034  pclfinclN  34037  diaelrnN  35135  docavalN  35213  dochval  35441  dvh4dimat  35528  dochexmidlem1  35550  lpolconN  35577  mapdordlem2  35727  ismrcd1  36062  ismrcd2  36063  ismrc  36065  mzpcompact2lem  36115  aomclem6  36430  hbtlem6  36501  rgspnval  36540  ssficl  36676  ssuncl  36677  ssdifcl  36678  sssymdifcl  36679  elmapintrab  36684  clcnvlem  36732  iunrelexpmin1  36802  iunrelexpmin2  36806  clsk3nimkb  37141  clsk1indlem1  37146  isotone1  37149  isotone2  37150  ntrclsiso  37168  gneispace  37235  gneispacess2  37247  onfrALTlem5  37561  onfrALTlem5VD  37926  islptre  38469  dvmptconst  38586  dvmptidg  38588  dvmulcncf  38598  dvdivcncf  38600  dvmptfprod  38618  stoweidlem51  38727  stoweidlem52  38728  fourierdlem103  38885  fourierdlem104  38886  ioorrnopnlem  38983  ioorrnopnxrlem  38985  salgenval  39000  ovnval2  39218  ovncvrrp  39237  ovnsubaddlem1  39243  ovnsubadd  39245  ovncvr2  39284  hspmbl  39302  lpvtx  40271  umgredgprv  40313  usgredgprvALT  40403  issubgr2  40477  subgrprop2  40479  egrsubgr  40482  0uhgrsubgr  40484  frcond3  41421
  Copyright terms: Public domain W3C validator