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

Theorem sseq1 3995
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 3985 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3977 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 482 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3977 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 481 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 213 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 218 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1530  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  sseq12  3997  sseq1i  3998  sseq1d  4001  nssne2  4031  psseq1  4067  uneqdifeq  4440  sbss  4464  pwjust  4542  elpwg  4547  elpwOLD  4550  elpwgOLD  4551  pwpw0  4744  sssn  4757  ssunsn2  4758  pwsnALT  4829  unimax  4871  trss  5177  al0ssb  5208  sseliALT  5209  elssabg  5235  intabs  5241  nnullss  5350  exss  5351  fri  5515  releq  5649  iss  5901  relcnvtrg  6116  fununi  6425  ssimaex  6744  isofrlem  7088  onssmin  7503  tfis  7560  tfisi  7564  funcnvuni  7627  ffoss  7641  f1oweALT  7667  frxp  7814  wfrlem1  7948  wfrlem4  7952  wfrlem15  7963  tfrlem1  8006  oawordeu  8174  qsss  8351  boxcutc  8497  sbthlem2  8620  sbth  8629  php  8693  isinf  8723  findcard2d  8752  unbnn2  8767  domunfican  8783  fiint  8787  finsschain  8823  indexfi  8824  dffi3  8887  hartogslem1  8998  cantnfval2  9124  cantnfle  9126  cantnflem1  9144  tz9.1  9163  setind  9168  tcvalg  9172  scott0  9307  bnd2  9314  carduni  9402  cardaleph  9507  alephinit  9513  aceq3lem  9538  dfac12lem3  9563  infmap2  9632  cflem  9660  cflm  9664  cflecard  9667  cfeq0  9670  cfsuc  9671  cfflb  9673  cfslb  9680  cfslb2n  9682  coftr  9687  fin23lem13  9746  fin23lem16  9749  fin23lem19  9750  fin23lem29  9755  fin1a2lem13  9826  itunitc  9835  domtriomlem  9856  axdc3lem2  9865  zorn2lem7  9916  zornn0g  9919  fpwwe2lem5  10048  pwfseqlem4a  10075  pwfseqlem4  10076  wunfi  10135  wunex2  10152  wuncval  10156  rankcf  10191  tskuni  10197  axgroth6  10242  axgroth3  10245  axgroth4  10246  fzoss1  13057  fsuppmapnn0fiubex  13353  hashf1lem2  13807  cleq1lem  14335  rtrclreclem4  14413  sumeq1  15038  fsumcvg3  15078  fsum2d  15118  fsumabs  15148  fsumrlim  15158  fsumo1  15159  fsumiun  15168  prodeq1f  15254  fprod2d  15327  lcmfunsnlem  15977  coprmprod  15997  vdwmc  16306  prmgaplem3  16381  prmgaplem4  16382  restsspw  16697  ismred2  16866  mrcval  16873  mrcuni  16884  acsfn  16922  isssc  17082  drsdirfi  17540  ipodrsima  17767  cntzssv  18390  pmtrfrn  18508  pmtrrn2  18510  pmtrdifellem1  18526  pmtrdifellem2  18527  sylow2alem2  18665  sylow2a  18666  efgval  18765  gsumzaddlem  18963  ablfac1eulem  19116  lspval  19669  lspindpi  19826  aspval  20023  mplsubglem  20135  mpllsslem  20136  mplcoe1  20166  mplcoe5  20169  znf1o  20616  zntoslem  20621  mdetunilem9  21147  uniopn  21423  fiinopn  21427  fiinbas  21478  baspartn  21480  eltg2  21484  eltg3  21488  topbas  21498  pptbas  21534  clsval  21563  neiint  21630  neips  21639  opnneissb  21640  opnssneib  21641  innei  21651  neiptoptop  21657  neiptopnei  21658  restbas  21684  restcld  21698  neitr  21706  restcls  21707  restntr  21708  cnpdis  21819  cmpsublem  21925  cmpsub  21926  fiuncmp  21930  unconn  21955  1stcfb  21971  2ndc1stc  21977  1stcrest  21979  2ndcctbss  21981  2ndcomap  21984  dis2ndc  21986  lly1stc  22022  refssex  22037  refun0  22041  llycmpkgen2  22076  txbas  22093  eltx  22094  ptuni2  22102  neitx  22133  ptpjopn  22138  ptcld  22139  txlm  22174  tx1stc  22176  txkgen  22178  xkopt  22181  xkococnlem  22185  ptcmpfi  22339  fbssfi  22363  opnfbas  22368  isfil2  22382  isfildlem  22383  snfil  22390  fsubbas  22393  ssfg  22398  fgss2  22400  fgcl  22404  fbasrn  22410  fgtr  22416  ufli  22440  uffix  22447  rnelfmlem  22478  fclscf  22551  alexsublem  22570  alexsubALTlem2  22574  alexsubALTlem3  22575  alexsubALTlem4  22576  alexsubALT  22577  tmdgsum2  22622  subgntr  22632  opnsubg  22633  qustgpopn  22645  tsmsfbas  22653  tsmsgsum  22664  tsmsres  22669  tsmsf1o  22670  tsmsxplem1  22678  tsmsxp  22680  isust  22729  ustssel  22731  ustincl  22733  ustdiag  22734  ustinvel  22735  ustexhalf  22736  ustexsym  22741  ust0  22745  restutop  22763  ustuqtop4  22770  utopsnneiplem  22773  blssexps  22953  blssex  22954  neibl  23028  blcld  23032  met1stc  23048  met2ndci  23049  metrest  23051  prdsxmslem2  23056  metustfbas  23084  cfilucfil  23086  metuel2  23092  metustbl  23093  restmetu  23097  dscopn  23100  isngp2  23123  tgioo  23321  tgqioo  23325  zdis  23341  xrge0tsms  23359  fsumcn  23395  volivth  24125  vitalilem2  24127  itgfsum  24344  limcun  24410  recnprss  24419  dvmptfsum  24489  ftc1a  24551  plyssc  24707  efopn  25156  jensen  25482  tglnunirn  26250  lpvtx  26769  umgredgprv  26808  usgredgprvALT  26893  issubgr2  26970  subgrprop2  26972  egrsubgr  26975  0uhgrsubgr  26977  frcond3  27964  hhsssh  28962  shintcl  29023  chintcl  29025  spanval  29026  omlsi  29097  pjoml  29129  chnlen0  29137  chsscon3  29193  chlejb1  29205  chnle  29207  spanun  29238  h1datom  29275  cmbr4i  29294  pjoml2  29304  pjoml3  29305  lecm  29310  osumcor2i  29337  osum  29338  spansncv  29346  pjcjt2  29385  pjopyth  29413  hstel2  29912  stj  29928  stcltr1i  29967  mdi  29988  mdbr3  29990  mdbr4  29991  dmdbr  29992  dmdmd  29993  dmdbr5  30001  mdsl1i  30014  mdslmd1lem3  30020  mdslmd1lem4  30021  mdslmd1i  30022  csmdsymi  30027  atss  30039  atom1d  30046  superpos  30047  chcv1  30048  shatomici  30051  shatomistici  30054  hatomistici  30055  chrelat2  30063  chirredi  30087  atcvat4i  30090  mdsymlem2  30097  mdsymlem6  30101  dmdbr6ati  30116  dmdbr7ati  30117  xrge0tsmsd  30608  gsumle  30641  gsumvsca1  30770  gsumvsca2  30771  prmidl  30865  tpr2rico  31043  issiga  31259  isrnsiga  31260  sigagenval  31287  measiuns  31364  dya2icoseg  31423  dya2iocnrect  31427  dya2iocuni  31429  carsgmon  31460  carsgsigalem  31461  carsgclctunlem2  31465  carsgclctun  31467  pmeasmono  31470  pmeasadd  31471  bnj517  32045  bnj1118  32142  bnj1145  32151  bnj1154  32157  bnj1452  32210  bnj1498  32219  pthhashvtx  32260  kur14lem1  32339  cvmopnlem  32411  dfon2lem3  32916  dfon2lem7  32920  frmin  32970  frrlem1  33009  frrlem13  33021  brsslt  33140  brsset  33236  fness  33583  fneref  33584  fnessref  33591  neibastop2lem  33594  topmeet  33598  fnejoin2  33603  tailfb  33611  filnetlem4  33615  onsucsuccmpi  33677  bj-snglss  34168  bj-restpw  34266  bj-imdirid  34356  dissneqlem  34492  relowlssretop  34515  relowlpssretop  34516  ctbssinf  34558  pibt2  34569  matunitlindflem1  34757  ptrecube  34761  poimirlem29  34790  mblfinlem2  34799  mblfinlem3  34800  mblfinlem4  34801  ismblfin  34802  ovoliunnfl  34803  voliunnfl  34805  volsupnfl  34806  indexa  34878  indexdom  34879  neificl  34898  istotbnd3  34919  sstotbnd2  34922  sstotbnd  34923  equivtotbnd  34926  ssbnd  34936  heiborlem1  34959  heiborlem6  34964  heiborlem8  34966  heiborlem10  34968  unichnidl  35179  pridl  35185  ismaxidl  35188  igenval  35209  igenval2  35214  ispridlc  35218  relcnveq3  35448  iss2  35471  elrelscnveq3  35600  brssr  35610  lsmsat  36013  lssatomic  36016  lssats  36017  lsat0cv  36038  lcvexchlem4  36042  lcvexchlem5  36043  lsatcvatlem  36054  l1cvpat  36059  ispsubsp  36750  linepsubN  36757  pclvalN  36895  ispsubclN  36942  ispsubcl2N  36952  pclfinclN  36955  diaelrnN  38050  docavalN  38128  dochval  38356  dvh4dimat  38443  dochexmidlem1  38465  lpolconN  38492  mapdordlem2  38642  ismrcd1  39162  ismrcd2  39163  ismrc  39165  mzpcompact2lem  39215  aomclem6  39526  hbtlem6  39596  rgspnval  39635  ssficl  39795  ssuncl  39796  ssdifcl  39797  sssymdifcl  39798  elmapintrab  39803  clcnvlem  39850  iunrelexpmin1  39920  iunrelexpmin2  39924  clsk3nimkb  40257  clsk1indlem1  40262  isotone1  40265  isotone2  40266  ntrclsiso  40284  gneispace  40351  gneispacess2  40363  onfrALTlem5  40743  onfrALTlem5VD  41086  islptre  41767  dvmptconst  42066  dvmptidg  42068  dvmulcncf  42077  dvdivcncf  42079  dvmptfprod  42097  stoweidlem51  42204  stoweidlem52  42205  fourierdlem103  42362  fourierdlem104  42363  ioorrnopnlem  42457  ioorrnopnxrlem  42459  salgenval  42474  ovnval2  42695  ovncvrrp  42714  ovnsubaddlem1  42720  ovnsubadd  42722  ovncvr2  42761  hspmbl  42779  uspgrsprfo  43857  setrec1lem1  44624  setrec1lem4  44627  setrec2fun  44629  elsetrecslem  44635  elpglem2  44648
  Copyright terms: Public domain W3C validator