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

Theorem sseq1 3989
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 3979 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3971 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 482 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3971 . . . 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 1528  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949
This theorem is referenced by:  sseq12  3991  sseq1i  3992  sseq1d  3995  nssne2  4025  psseq1  4061  uneqdifeq  4434  sbss  4458  pwjust  4536  elpwg  4541  elpwOLD  4544  elpwgOLD  4545  pwpw0  4738  sssn  4751  ssunsn2  4752  pwsnALT  4823  unimax  4865  trss  5172  al0ssb  5203  sseliALT  5204  elssabg  5230  intabs  5236  nnullss  5345  exss  5346  fri  5510  releq  5644  iss  5896  relcnvtrg  6112  fununi  6422  ssimaex  6741  isofrlem  7082  onssmin  7501  tfis  7558  tfisi  7562  funcnvuni  7625  ffoss  7636  f1oweALT  7662  frxp  7809  wfrlem1  7943  wfrlem4  7947  wfrlem15  7958  tfrlem1  8001  oawordeu  8170  qsss  8347  boxcutc  8493  sbthlem2  8616  sbth  8625  php  8689  isinf  8719  findcard2d  8748  unbnn2  8763  domunfican  8779  fiint  8783  finsschain  8819  indexfi  8820  dffi3  8883  hartogslem1  8994  cantnfval2  9120  cantnfle  9122  cantnflem1  9140  tz9.1  9159  setind  9164  tcvalg  9168  scott0  9303  bnd2  9310  carduni  9398  cardaleph  9503  alephinit  9509  aceq3lem  9534  dfac12lem3  9559  infmap2  9628  cflem  9656  cflm  9660  cflecard  9663  cfeq0  9666  cfsuc  9667  cfflb  9669  cfslb  9676  cfslb2n  9678  coftr  9683  fin23lem13  9742  fin23lem16  9745  fin23lem19  9746  fin23lem29  9751  fin1a2lem13  9822  itunitc  9831  domtriomlem  9852  axdc3lem2  9861  zorn2lem7  9912  zornn0g  9915  fpwwe2lem5  10044  pwfseqlem4a  10071  pwfseqlem4  10072  wunfi  10131  wunex2  10148  wuncval  10152  rankcf  10187  tskuni  10193  axgroth6  10238  axgroth3  10241  axgroth4  10242  fzoss1  13052  fsuppmapnn0fiubex  13348  hashf1lem2  13802  cleq1lem  14330  rtrclreclem4  14408  sumeq1  15033  fsumcvg3  15074  fsum2d  15114  fsumabs  15144  fsumrlim  15154  fsumo1  15155  fsumiun  15164  prodeq1f  15250  fprod2d  15323  lcmfunsnlem  15973  coprmprod  15993  vdwmc  16302  prmgaplem3  16377  prmgaplem4  16378  restsspw  16693  ismred2  16862  mrcval  16869  mrcuni  16880  acsfn  16918  isssc  17078  drsdirfi  17536  ipodrsima  17763  cntzssv  18396  pmtrfrn  18515  pmtrrn2  18517  pmtrdifellem1  18533  pmtrdifellem2  18534  sylow2alem2  18672  sylow2a  18673  efgval  18772  gsumzaddlem  18970  ablfac1eulem  19123  lspval  19676  lspindpi  19833  aspval  20030  mplsubglem  20142  mpllsslem  20143  mplcoe1  20174  mplcoe5  20177  znf1o  20626  zntoslem  20631  mdetunilem9  21157  uniopn  21433  fiinopn  21437  fiinbas  21488  baspartn  21490  eltg2  21494  eltg3  21498  topbas  21508  pptbas  21544  clsval  21573  neiint  21640  neips  21649  opnneissb  21650  opnssneib  21651  innei  21661  neiptoptop  21667  neiptopnei  21668  restbas  21694  restcld  21708  neitr  21716  restcls  21717  restntr  21718  cnpdis  21829  cmpsublem  21935  cmpsub  21936  fiuncmp  21940  unconn  21965  1stcfb  21981  2ndc1stc  21987  1stcrest  21989  2ndcctbss  21991  2ndcomap  21994  dis2ndc  21996  lly1stc  22032  refssex  22047  refun0  22051  llycmpkgen2  22086  txbas  22103  eltx  22104  ptuni2  22112  neitx  22143  ptpjopn  22148  ptcld  22149  txlm  22184  tx1stc  22186  txkgen  22188  xkopt  22191  xkococnlem  22195  ptcmpfi  22349  fbssfi  22373  opnfbas  22378  isfil2  22392  isfildlem  22393  snfil  22400  fsubbas  22403  ssfg  22408  fgss2  22410  fgcl  22414  fbasrn  22420  fgtr  22426  ufli  22450  uffix  22457  rnelfmlem  22488  fclscf  22561  alexsublem  22580  alexsubALTlem2  22584  alexsubALTlem3  22585  alexsubALTlem4  22586  alexsubALT  22587  tmdgsum2  22632  subgntr  22642  opnsubg  22643  qustgpopn  22655  tsmsfbas  22663  tsmsgsum  22674  tsmsres  22679  tsmsf1o  22680  tsmsxplem1  22688  tsmsxp  22690  isust  22739  ustssel  22741  ustincl  22743  ustdiag  22744  ustinvel  22745  ustexhalf  22746  ustexsym  22751  ust0  22755  restutop  22773  ustuqtop4  22780  utopsnneiplem  22783  blssexps  22963  blssex  22964  neibl  23038  blcld  23042  met1stc  23058  met2ndci  23059  metrest  23061  prdsxmslem2  23066  metustfbas  23094  cfilucfil  23096  metuel2  23102  metustbl  23103  restmetu  23107  dscopn  23110  isngp2  23133  tgioo  23331  tgqioo  23335  zdis  23351  xrge0tsms  23369  fsumcn  23405  volivth  24135  vitalilem2  24137  itgfsum  24354  limcun  24420  recnprss  24429  dvmptfsum  24499  ftc1a  24561  plyssc  24717  efopn  25168  jensen  25493  tglnunirn  26261  lpvtx  26780  umgredgprv  26819  usgredgprvALT  26904  issubgr2  26981  subgrprop2  26983  egrsubgr  26986  0uhgrsubgr  26988  frcond3  27975  hhsssh  28973  shintcl  29034  chintcl  29036  spanval  29037  omlsi  29108  pjoml  29140  chnlen0  29148  chsscon3  29204  chlejb1  29216  chnle  29218  spanun  29249  h1datom  29286  cmbr4i  29305  pjoml2  29315  pjoml3  29316  lecm  29321  osumcor2i  29348  osum  29349  spansncv  29357  pjcjt2  29396  pjopyth  29424  hstel2  29923  stj  29939  stcltr1i  29978  mdi  29999  mdbr3  30001  mdbr4  30002  dmdbr  30003  dmdmd  30004  dmdbr5  30012  mdsl1i  30025  mdslmd1lem3  30031  mdslmd1lem4  30032  mdslmd1i  30033  csmdsymi  30038  atss  30050  atom1d  30057  superpos  30058  chcv1  30059  shatomici  30062  shatomistici  30065  hatomistici  30066  chrelat2  30074  chirredi  30098  atcvat4i  30101  mdsymlem2  30108  mdsymlem6  30112  dmdbr6ati  30127  dmdbr7ati  30128  xrge0tsmsd  30619  gsumle  30652  gsumvsca1  30781  gsumvsca2  30782  prmidl  30876  tpr2rico  31054  issiga  31270  isrnsiga  31271  sigagenval  31298  measiuns  31375  dya2icoseg  31434  dya2iocnrect  31438  dya2iocuni  31440  carsgmon  31471  carsgsigalem  31472  carsgclctunlem2  31476  carsgclctun  31478  pmeasmono  31481  pmeasadd  31482  bnj517  32056  bnj1118  32153  bnj1145  32162  bnj1154  32168  bnj1452  32221  bnj1498  32230  pthhashvtx  32271  kur14lem1  32350  cvmopnlem  32422  dfon2lem3  32927  dfon2lem7  32931  frmin  32981  frrlem1  33020  frrlem13  33032  brsslt  33151  brsset  33247  fness  33594  fneref  33595  fnessref  33602  neibastop2lem  33605  topmeet  33609  fnejoin2  33614  tailfb  33622  filnetlem4  33626  onsucsuccmpi  33688  bj-snglss  34179  bj-restpw  34277  bj-imdirid  34367  dissneqlem  34503  relowlssretop  34526  relowlpssretop  34527  ctbssinf  34569  pibt2  34580  matunitlindflem1  34769  ptrecube  34773  poimirlem29  34802  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  ovoliunnfl  34815  voliunnfl  34817  volsupnfl  34818  indexa  34889  indexdom  34890  neificl  34909  istotbnd3  34930  sstotbnd2  34933  sstotbnd  34934  equivtotbnd  34937  ssbnd  34947  heiborlem1  34970  heiborlem6  34975  heiborlem8  34977  heiborlem10  34979  unichnidl  35190  pridl  35196  ismaxidl  35199  igenval  35220  igenval2  35225  ispridlc  35229  relcnveq3  35459  iss2  35482  elrelscnveq3  35611  brssr  35621  lsmsat  36024  lssatomic  36027  lssats  36028  lsat0cv  36049  lcvexchlem4  36053  lcvexchlem5  36054  lsatcvatlem  36065  l1cvpat  36070  ispsubsp  36761  linepsubN  36768  pclvalN  36906  ispsubclN  36953  ispsubcl2N  36963  pclfinclN  36966  diaelrnN  38061  docavalN  38139  dochval  38367  dvh4dimat  38454  dochexmidlem1  38476  lpolconN  38503  mapdordlem2  38653  ismrcd1  39173  ismrcd2  39174  ismrc  39176  mzpcompact2lem  39226  aomclem6  39537  hbtlem6  39607  rgspnval  39646  ssficl  39806  ssuncl  39807  ssdifcl  39808  sssymdifcl  39809  elmapintrab  39814  clcnvlem  39861  iunrelexpmin1  39931  iunrelexpmin2  39935  clsk3nimkb  40268  clsk1indlem1  40273  isotone1  40276  isotone2  40277  ntrclsiso  40295  gneispace  40362  gneispacess2  40374  onfrALTlem5  40753  onfrALTlem5VD  41096  islptre  41776  dvmptconst  42075  dvmptidg  42077  dvmulcncf  42086  dvdivcncf  42088  dvmptfprod  42106  stoweidlem51  42213  stoweidlem52  42214  fourierdlem103  42371  fourierdlem104  42372  ioorrnopnlem  42466  ioorrnopnxrlem  42468  salgenval  42483  ovnval2  42704  ovncvrrp  42723  ovnsubaddlem1  42729  ovnsubadd  42731  ovncvr2  42770  hspmbl  42788  elsetpreimafvssdm  43423  uspgrsprfo  43900  setrec1lem1  44718  setrec1lem4  44721  setrec2fun  44723  elsetrecslem  44729  elpglem2  44742
  Copyright terms: Public domain W3C validator