MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseq12d Unicode version

Theorem sseq12d 3532
Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)
Hypotheses
Ref Expression
sseq1d.1
sseq12d.2
Assertion
Ref Expression
sseq12d

Proof of Theorem sseq12d
StepHypRef Expression
1 sseq1d.1 . . 3
21sseq1d 3530 . 2
3 sseq12d.2 . . 3
43sseq2d 3531 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  C_wss 3475
This theorem is referenced by:  3sstr3d  3545  3sstr4d  3546  ssdifeq0  3910  relcnvtr  5532  knatar  6253  suppfnss  6944  funsssuppss  6945  smogt  7057  oawordri  7218  omwordi  7239  omwordri  7240  oewordi  7259  oewordri  7260  oeworde  7261  nnawordi  7289  nnmwordi  7303  nnmwordri  7304  sbthlem2  7648  sbth  7657  marypha2lem3  7917  hartogslem1  7988  inf3lem1  8066  tcrank  8323  alephle  8490  cfsmolem  8671  isfin3ds  8730  fin23lem17  8739  fin23lem39  8751  isf32lem1  8754  isf32lem2  8755  isf32lem11  8764  isf33lem  8767  isf34lem7  8780  isf34lem6  8781  fin1a2lem13  8813  itunitc1  8821  dominf  8846  dcomex  8848  axdc2lem  8849  dominfac  8969  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwecbv  9043  fpwwelem  9044  canthwelem  9049  canthwe  9050  wunex2  9137  swrdval  12644  vdwpc  14498  vdwlem1  14499  vdwlem6  14504  vdwlem7  14505  vdwlem8  14506  isstruct2  14641  ressval  14684  mreexexlemd  15041  isacs1i  15054  isssc  15189  ssc2  15191  fullfunc  15275  fthfunc  15276  isps  15832  istsr  15847  isdir  15862  gsumvalx  15897  efgi2  16743  dmdprd  17029  dprdss  17076  dmdprdpr  17098  scmatdmat  19017  basis1  19451  baspartn  19455  eltg  19458  cncls  19775  ispnrm  19840  1stcfb  19946  2ndcctbss  19956  1stcelcls  19962  subislly  19982  kgenidm  20048  ptpjpre1  20072  txcmplem2  20143  flimval  20464  flimcf  20483  fclscf  20526  metss  21011  isngp  21116  iscph  21617  equivcau  21739  caubl  21746  caublcls  21747  ovoliunlem3  21915  volsuplem  21965  volsup  21966  dyaddisj  22005  itg1climres  22121  edgss  24352  isausgra  24354  cusgrafilem1  24479  issh  26125  isch  26140  hsupss  26259  shslej  26298  shlub  26332  ledi  26458  pjoi0  26635  mdbr4  27217  dmdbr4  27225  dmdi4  27226  dmdbr5  27227  mdslle1i  27236  mdslle2i  27237  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd1lem3  27246  mdslmd1lem4  27247  mdslmd1i  27248  sumdmdlem2  27338  resvval  27817  zhmnrg  27948  cvmliftlem3  28732  ismfs  28909  dfrtrcl2  29071  volsupnfl  30059  ismrcd1  30630  ismrcd2  30631  ismrc  30633  incssnn0  30643  diophrw  30692  hbtlem5  31077  hbt  31079  nzss  31222  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  scmsuppss  32965  lssatle  34740  pmaple  35485  2polcon4bN  35642  ispautN  35823  diaord  36774  dibord  36886  dihord6apre  36983  dihord3  36984  dihord4  36985  dihcnvord  37001  dvh4dimlem  37170  islpolN  37210  mapdordlem2  37364  mapdcnvordN  37385  mapdindp  37398  hdmaplkr  37643  trficl  37779  trclub  37784  trclubg  37785  heeq12  37800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator