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

Theorem sseq1 3659
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 3651 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
2 sstr2 3643 . . . 4 (𝐵𝐴 → (𝐴𝐶𝐵𝐶))
32adantl 481 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
4 sstr2 3643 . . . 4 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
54adantr 480 . . 3 ((𝐴𝐵𝐵𝐴) → (𝐵𝐶𝐴𝐶))
63, 5impbid 202 . 2 ((𝐴𝐵𝐵𝐴) → (𝐴𝐶𝐵𝐶))
71, 6sylbi 207 1 (𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  sseq12  3661  sseq1i  3662  sseq1d  3665  nssne2  3695  psseq1  3727  uneqdifeq  4090  uneqdifeqOLD  4091  sbss  4117  pwjust  4192  elpw  4197  elpwg  4199  pwpw0  4376  sssn  4390  ssunsn2  4391  pwsnALT  4461  unimax  4505  trss  4794  trssOLD  4795  sseliALT  4824  elssabg  4849  intabs  4855  nnullss  4960  exss  4961  fri  5105  releq  5235  iss  5482  relcnvtr  5693  fununi  6002  ssimaex  6302  isofrlem  6630  onssmin  7039  tfis  7096  tfisi  7100  funcnvuni  7161  ffoss  7169  f1oweALT  7194  frxp  7332  wfrlem1  7459  wfrlem4  7463  wfrlem15  7474  tfrlem1  7517  oawordeu  7680  qsss  7851  boxcutc  7993  sbthlem2  8112  sbth  8121  php  8185  isinf  8214  findcard2d  8243  unbnn2  8258  domunfican  8274  fiint  8278  finsschain  8314  indexfi  8315  dffi3  8378  hartogslem1  8488  cantnfval2  8604  cantnfle  8606  cantnflem1  8624  tz9.1  8643  setind  8648  tcvalg  8652  scott0  8787  bnd2  8794  carduni  8845  cardaleph  8950  alephinit  8956  aceq3lem  8981  dfac12lem3  9005  infmap2  9078  cflem  9106  cflm  9110  cflecard  9113  cfeq0  9116  cfsuc  9117  cfflb  9119  cfslb  9126  cfslb2n  9128  coftr  9133  fin23lem13  9192  fin23lem16  9195  fin23lem19  9196  fin23lem29  9201  fin1a2lem13  9272  itunitc  9281  domtriomlem  9302  axdc3lem2  9311  zorn2lem7  9362  zornn0g  9365  fpwwe2lem5  9494  pwfseqlem4a  9521  pwfseqlem4  9522  wunfi  9581  wunex2  9598  wuncval  9602  rankcf  9637  tskuni  9643  axgroth6  9688  axgroth3  9691  axgroth4  9692  fzoss1  12534  fsuppmapnn0fiubex  12832  hashf1lem2  13278  cleq1lem  13767  rtrclreclem4  13845  sumeq1  14463  fsumcvg3  14504  fsum2d  14546  fsumabs  14577  fsumrlim  14587  fsumo1  14588  fsumiun  14597  prodeq1f  14682  fprod2d  14755  lcmfunsnlem  15401  coprmprod  15422  vdwmc  15729  prmgaplem3  15804  prmgaplem4  15805  restsspw  16139  ismred2  16310  mrcval  16317  mrcuni  16328  acsfn  16367  isssc  16527  drsdirfi  16985  ipodrsima  17212  cntzssv  17807  pmtrfrn  17924  pmtrrn2  17926  pmtrdifellem1  17942  pmtrdifellem2  17943  isslw  18069  sylow2alem2  18079  sylow2a  18080  efgval  18176  gsumzaddlem  18367  ablfac1eulem  18517  lspval  19023  lspindpi  19180  aspval  19376  mplsubglem  19482  mpllsslem  19483  mplcoe1  19513  mplcoe5  19516  znf1o  19948  zntoslem  19953  mdetunilem9  20474  uniopn  20750  fiinopn  20754  fiinbas  20804  baspartn  20806  eltg2  20810  eltg3  20814  topbas  20824  pptbas  20860  clsval  20889  neival  20954  neiint  20956  neips  20965  opnneissb  20966  opnssneib  20967  innei  20977  neiptoptop  20983  neiptopnei  20984  restbas  21010  restcld  21024  neitr  21032  restcls  21033  restntr  21034  cnpdis  21145  cmpsublem  21250  cmpsub  21251  fiuncmp  21255  unconn  21280  1stcfb  21296  2ndc1stc  21302  1stcrest  21304  2ndcctbss  21306  2ndcomap  21309  dis2ndc  21311  lly1stc  21347  refssex  21362  refun0  21366  llycmpkgen2  21401  txbas  21418  eltx  21419  ptuni2  21427  neitx  21458  ptpjopn  21463  ptcld  21464  txlm  21499  tx1stc  21501  txkgen  21503  xkopt  21506  xkococnlem  21510  ptcmpfi  21664  fbssfi  21688  opnfbas  21693  isfil2  21707  isfildlem  21708  snfil  21715  fsubbas  21718  ssfg  21723  fgss2  21725  fgcl  21729  fbasrn  21735  fgtr  21741  ufli  21765  uffix  21772  rnelfmlem  21803  fclscf  21876  alexsublem  21895  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  alexsubALT  21902  tmdgsum2  21947  subgntr  21957  opnsubg  21958  qustgpopn  21970  tsmsfbas  21978  tsmsgsum  21989  tsmsres  21994  tsmsf1o  21995  tsmsxplem1  22003  tsmsxp  22005  isust  22054  ustssel  22056  ustincl  22058  ustdiag  22059  ustinvel  22060  ustexhalf  22061  ustexsym  22066  ust0  22070  restutop  22088  ustuqtop4  22095  utopsnneiplem  22098  blssexps  22278  blssex  22279  neibl  22353  blcld  22357  met1stc  22373  met2ndci  22374  metrest  22376  prdsxmslem2  22381  metustfbas  22409  cfilucfil  22411  metuel2  22417  metustbl  22418  restmetu  22422  dscopn  22425  isngp2  22448  tgioo  22646  tgqioo  22650  zdis  22666  xrge0tsms  22684  fsumcn  22720  ovolval  23288  volivth  23421  vitalilem2  23423  itgfsum  23638  limcun  23704  recnprss  23713  dvmptfsum  23783  ftc1a  23845  plyssc  24001  efopn  24449  jensen  24760  tglnunirn  25488  lpvtx  26008  umgredgprv  26047  usgredgprvALT  26132  issubgr2  26209  subgrprop2  26211  egrsubgr  26214  0uhgrsubgr  26216  frcond3  27249  hhsssh  28254  shintcl  28317  chintcl  28319  spanval  28320  omlsi  28391  pjoml  28423  chnlen0  28431  chsscon3  28487  chlejb1  28499  chnle  28501  spanun  28532  h1datom  28569  cmbr4i  28588  pjoml2  28598  pjoml3  28599  lecm  28604  osumcor2i  28631  osum  28632  spansncv  28640  pjcjt2  28679  pjopyth  28707  hstel2  29206  stj  29222  stcltr1i  29261  mdi  29282  mdbr3  29284  mdbr4  29285  dmdbr  29286  dmdmd  29287  dmdbr5  29295  mdsl1i  29308  mdslmd1lem3  29314  mdslmd1lem4  29315  mdslmd1i  29316  csmdsymi  29321  atss  29333  atom1d  29340  superpos  29341  chcv1  29342  shatomici  29345  shatomistici  29348  hatomistici  29349  chrelat2  29357  chirredi  29381  atcvat4i  29384  mdsymlem2  29391  mdsymlem6  29395  dmdbr6ati  29410  dmdbr7ati  29411  gsumle  29907  gsumvsca1  29910  gsumvsca2  29911  xrge0tsmsd  29913  tpr2rico  30086  issiga  30302  isrnsigaOLD  30303  isrnsiga  30304  sigagenval  30331  measiuns  30408  dya2icoseg  30467  dya2iocnrect  30471  dya2iocuni  30473  carsgmon  30504  carsgsigalem  30505  carsgclctunlem2  30509  carsgclctun  30511  pmeasmono  30514  pmeasadd  30515  bnj517  31081  bnj1118  31178  bnj1145  31187  bnj1154  31193  bnj1452  31246  bnj1498  31255  kur14lem1  31314  cvmopnlem  31386  dfon2lem3  31814  dfon2lem7  31818  frmin  31867  frrlem1  31905  brsslt  32025  brsset  32121  fness  32469  fneref  32470  fnessref  32477  neibastop2lem  32480  topmeet  32484  fnejoin2  32489  tailfb  32497  filnetlem4  32501  onsucsuccmpi  32567  bj-snglss  33083  bj-restpw  33170  dissneqlem  33317  relowlssretop  33341  relowlpssretop  33342  matunitlindflem1  33535  ptrecube  33539  poimirlem29  33568  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  indexa  33658  indexdom  33659  neificl  33679  istotbnd3  33700  sstotbnd2  33703  sstotbnd  33704  equivtotbnd  33707  ssbnd  33717  heiborlem1  33740  heiborlem6  33745  heiborlem8  33747  heiborlem10  33749  unichnidl  33960  pridl  33966  ismaxidl  33969  igenval  33990  igenval2  33995  ispridlc  33999  relcnveq3  34233  iss2  34252  elrelscnveq3  34381  brssr  34391  lsmsat  34613  lssatomic  34616  lssats  34617  lsat0cv  34638  lcvexchlem4  34642  lcvexchlem5  34643  lsatcvatlem  34654  l1cvpat  34659  ispsubsp  35349  linepsubN  35356  pclvalN  35494  ispsubclN  35541  ispsubcl2N  35551  pclfinclN  35554  diaelrnN  36651  docavalN  36729  dochval  36957  dvh4dimat  37044  dochexmidlem1  37066  lpolconN  37093  mapdordlem2  37243  ismrcd1  37578  ismrcd2  37579  ismrc  37581  mzpcompact2lem  37631  aomclem6  37946  hbtlem6  38016  rgspnval  38055  ssficl  38191  ssuncl  38192  ssdifcl  38193  sssymdifcl  38194  elmapintrab  38199  clcnvlem  38247  iunrelexpmin1  38317  iunrelexpmin2  38321  clsk3nimkb  38655  clsk1indlem1  38660  isotone1  38663  isotone2  38664  ntrclsiso  38682  gneispace  38749  gneispacess2  38761  onfrALTlem5  39074  onfrALTlem5VD  39435  islptre  40169  dvmptconst  40447  dvmptidg  40449  dvmulcncf  40458  dvdivcncf  40460  dvmptfprod  40478  stoweidlem51  40586  stoweidlem52  40587  fourierdlem103  40744  fourierdlem104  40745  ioorrnopnlem  40842  ioorrnopnxrlem  40844  salgenval  40859  ovnval2  41080  ovncvrrp  41099  ovnsubaddlem1  41105  ovnsubadd  41107  ovncvr2  41146  hspmbl  41164  uspgrsprfo  42081  setrec1lem1  42759  setrec1lem4  42762  setrec2fun  42764  elsetrecslem  42770  elpglem2  42783
  Copyright terms: Public domain W3C validator