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

Theorem sseq1 3991
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 3981 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3973 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 482 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3973 . . . 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 3935
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  sseq12  3993  sseq1i  3994  sseq1d  3997  nssne2  4027  psseq1  4063  uneqdifeq  4436  sbss  4460  pwjust  4538  elpwg  4543  elpwOLD  4546  elpwgOLD  4547  pwpw0  4740  sssn  4753  ssunsn2  4754  pwsnALT  4825  unimax  4867  trss  5173  al0ssb  5204  sseliALT  5205  elssabg  5231  intabs  5237  nnullss  5346  exss  5347  fri  5511  releq  5645  iss  5897  relcnvtrg  6113  fununi  6423  ssimaex  6742  isofrlem  7082  onssmin  7500  tfis  7557  tfisi  7561  funcnvuni  7624  ffoss  7638  f1oweALT  7664  frxp  7811  wfrlem1  7945  wfrlem4  7949  wfrlem15  7960  tfrlem1  8003  oawordeu  8171  qsss  8348  boxcutc  8494  sbthlem2  8617  sbth  8626  php  8690  isinf  8720  findcard2d  8749  unbnn2  8764  domunfican  8780  fiint  8784  finsschain  8820  indexfi  8821  dffi3  8884  hartogslem1  8995  cantnfval2  9121  cantnfle  9123  cantnflem1  9141  tz9.1  9160  setind  9165  tcvalg  9169  scott0  9304  bnd2  9311  carduni  9399  cardaleph  9504  alephinit  9510  aceq3lem  9535  dfac12lem3  9560  infmap2  9629  cflem  9657  cflm  9661  cflecard  9664  cfeq0  9667  cfsuc  9668  cfflb  9670  cfslb  9677  cfslb2n  9679  coftr  9684  fin23lem13  9743  fin23lem16  9746  fin23lem19  9747  fin23lem29  9752  fin1a2lem13  9823  itunitc  9832  domtriomlem  9853  axdc3lem2  9862  zorn2lem7  9913  zornn0g  9916  fpwwe2lem5  10045  pwfseqlem4a  10072  pwfseqlem4  10073  wunfi  10132  wunex2  10149  wuncval  10153  rankcf  10188  tskuni  10194  axgroth6  10239  axgroth3  10242  axgroth4  10243  fzoss1  13054  fsuppmapnn0fiubex  13350  hashf1lem2  13804  cleq1lem  14332  rtrclreclem4  14410  sumeq1  15035  fsumcvg3  15076  fsum2d  15116  fsumabs  15146  fsumrlim  15156  fsumo1  15157  fsumiun  15166  prodeq1f  15252  fprod2d  15325  lcmfunsnlem  15975  coprmprod  15995  vdwmc  16304  prmgaplem3  16379  prmgaplem4  16380  restsspw  16695  ismred2  16864  mrcval  16871  mrcuni  16882  acsfn  16920  isssc  17080  drsdirfi  17538  ipodrsima  17765  cntzssv  18398  pmtrfrn  18517  pmtrrn2  18519  pmtrdifellem1  18535  pmtrdifellem2  18536  sylow2alem2  18674  sylow2a  18675  efgval  18774  gsumzaddlem  18972  ablfac1eulem  19125  lspval  19678  lspindpi  19835  aspval  20032  mplsubglem  20144  mpllsslem  20145  mplcoe1  20176  mplcoe5  20179  znf1o  20628  zntoslem  20633  mdetunilem9  21159  uniopn  21435  fiinopn  21439  fiinbas  21490  baspartn  21492  eltg2  21496  eltg3  21500  topbas  21510  pptbas  21546  clsval  21575  neiint  21642  neips  21651  opnneissb  21652  opnssneib  21653  innei  21663  neiptoptop  21669  neiptopnei  21670  restbas  21696  restcld  21710  neitr  21718  restcls  21719  restntr  21720  cnpdis  21831  cmpsublem  21937  cmpsub  21938  fiuncmp  21942  unconn  21967  1stcfb  21983  2ndc1stc  21989  1stcrest  21991  2ndcctbss  21993  2ndcomap  21996  dis2ndc  21998  lly1stc  22034  refssex  22049  refun0  22053  llycmpkgen2  22088  txbas  22105  eltx  22106  ptuni2  22114  neitx  22145  ptpjopn  22150  ptcld  22151  txlm  22186  tx1stc  22188  txkgen  22190  xkopt  22193  xkococnlem  22197  ptcmpfi  22351  fbssfi  22375  opnfbas  22380  isfil2  22394  isfildlem  22395  snfil  22402  fsubbas  22405  ssfg  22410  fgss2  22412  fgcl  22416  fbasrn  22422  fgtr  22428  ufli  22452  uffix  22459  rnelfmlem  22490  fclscf  22563  alexsublem  22582  alexsubALTlem2  22586  alexsubALTlem3  22587  alexsubALTlem4  22588  alexsubALT  22589  tmdgsum2  22634  subgntr  22644  opnsubg  22645  qustgpopn  22657  tsmsfbas  22665  tsmsgsum  22676  tsmsres  22681  tsmsf1o  22682  tsmsxplem1  22690  tsmsxp  22692  isust  22741  ustssel  22743  ustincl  22745  ustdiag  22746  ustinvel  22747  ustexhalf  22748  ustexsym  22753  ust0  22757  restutop  22775  ustuqtop4  22782  utopsnneiplem  22785  blssexps  22965  blssex  22966  neibl  23040  blcld  23044  met1stc  23060  met2ndci  23061  metrest  23063  prdsxmslem2  23068  metustfbas  23096  cfilucfil  23098  metuel2  23104  metustbl  23105  restmetu  23109  dscopn  23112  isngp2  23135  tgioo  23333  tgqioo  23337  zdis  23353  xrge0tsms  23371  fsumcn  23407  volivth  24137  vitalilem2  24139  itgfsum  24356  limcun  24422  recnprss  24431  dvmptfsum  24501  ftc1a  24563  plyssc  24719  efopn  25168  jensen  25494  tglnunirn  26262  lpvtx  26781  umgredgprv  26820  usgredgprvALT  26905  issubgr2  26982  subgrprop2  26984  egrsubgr  26987  0uhgrsubgr  26989  frcond3  27976  hhsssh  28974  shintcl  29035  chintcl  29037  spanval  29038  omlsi  29109  pjoml  29141  chnlen0  29149  chsscon3  29205  chlejb1  29217  chnle  29219  spanun  29250  h1datom  29287  cmbr4i  29306  pjoml2  29316  pjoml3  29317  lecm  29322  osumcor2i  29349  osum  29350  spansncv  29358  pjcjt2  29397  pjopyth  29425  hstel2  29924  stj  29940  stcltr1i  29979  mdi  30000  mdbr3  30002  mdbr4  30003  dmdbr  30004  dmdmd  30005  dmdbr5  30013  mdsl1i  30026  mdslmd1lem3  30032  mdslmd1lem4  30033  mdslmd1i  30034  csmdsymi  30039  atss  30051  atom1d  30058  superpos  30059  chcv1  30060  shatomici  30063  shatomistici  30066  hatomistici  30067  chrelat2  30075  chirredi  30099  atcvat4i  30102  mdsymlem2  30109  mdsymlem6  30113  dmdbr6ati  30128  dmdbr7ati  30129  xrge0tsmsd  30620  gsumle  30653  gsumvsca1  30782  gsumvsca2  30783  prmidl  30877  tpr2rico  31055  issiga  31271  isrnsiga  31272  sigagenval  31299  measiuns  31376  dya2icoseg  31435  dya2iocnrect  31439  dya2iocuni  31441  carsgmon  31472  carsgsigalem  31473  carsgclctunlem2  31477  carsgclctun  31479  pmeasmono  31482  pmeasadd  31483  bnj517  32057  bnj1118  32154  bnj1145  32163  bnj1154  32169  bnj1452  32222  bnj1498  32231  pthhashvtx  32272  kur14lem1  32351  cvmopnlem  32423  dfon2lem3  32928  dfon2lem7  32932  frmin  32982  frrlem1  33021  frrlem13  33033  brsslt  33152  brsset  33248  fness  33595  fneref  33596  fnessref  33603  neibastop2lem  33606  topmeet  33610  fnejoin2  33615  tailfb  33623  filnetlem4  33627  onsucsuccmpi  33689  bj-snglss  34180  bj-restpw  34278  bj-imdirid  34368  dissneqlem  34504  relowlssretop  34527  relowlpssretop  34528  ctbssinf  34570  pibt2  34581  matunitlindflem1  34770  ptrecube  34774  poimirlem29  34803  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  ovoliunnfl  34816  voliunnfl  34818  volsupnfl  34819  indexa  34891  indexdom  34892  neificl  34911  istotbnd3  34932  sstotbnd2  34935  sstotbnd  34936  equivtotbnd  34939  ssbnd  34949  heiborlem1  34972  heiborlem6  34977  heiborlem8  34979  heiborlem10  34981  unichnidl  35192  pridl  35198  ismaxidl  35201  igenval  35222  igenval2  35227  ispridlc  35231  relcnveq3  35461  iss2  35484  elrelscnveq3  35613  brssr  35623  lsmsat  36026  lssatomic  36029  lssats  36030  lsat0cv  36051  lcvexchlem4  36055  lcvexchlem5  36056  lsatcvatlem  36067  l1cvpat  36072  ispsubsp  36763  linepsubN  36770  pclvalN  36908  ispsubclN  36955  ispsubcl2N  36965  pclfinclN  36968  diaelrnN  38063  docavalN  38141  dochval  38369  dvh4dimat  38456  dochexmidlem1  38478  lpolconN  38505  mapdordlem2  38655  ismrcd1  39175  ismrcd2  39176  ismrc  39178  mzpcompact2lem  39228  aomclem6  39539  hbtlem6  39609  rgspnval  39648  ssficl  39808  ssuncl  39809  ssdifcl  39810  sssymdifcl  39811  elmapintrab  39816  clcnvlem  39863  iunrelexpmin1  39933  iunrelexpmin2  39937  clsk3nimkb  40270  clsk1indlem1  40275  isotone1  40278  isotone2  40279  ntrclsiso  40297  gneispace  40364  gneispacess2  40376  onfrALTlem5  40756  onfrALTlem5VD  41099  islptre  41780  dvmptconst  42079  dvmptidg  42081  dvmulcncf  42090  dvdivcncf  42092  dvmptfprod  42110  stoweidlem51  42217  stoweidlem52  42218  fourierdlem103  42375  fourierdlem104  42376  ioorrnopnlem  42470  ioorrnopnxrlem  42472  salgenval  42487  ovnval2  42708  ovncvrrp  42727  ovnsubaddlem1  42733  ovnsubadd  42735  ovncvr2  42774  hspmbl  42792  uspgrsprfo  43870  setrec1lem1  44688  setrec1lem4  44691  setrec2fun  44693  elsetrecslem  44699  elpglem2  44712
  Copyright terms: Public domain W3C validator