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

Theorem ssexd 4563
Description: A subclass of a set is a set. Deduction form of ssexg 4562. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
ssexd.1  |-  ( ph  ->  B  e.  C )
ssexd.2  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
ssexd  |-  ( ph  ->  A  e.  _V )

Proof of Theorem ssexd
StepHypRef Expression
1 ssexd.2 . 2  |-  ( ph  ->  A  C_  B )
2 ssexd.1 . 2  |-  ( ph  ->  B  e.  C )
3 ssexg 4562 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 665 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   _Vcvv 3078    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-in 3440  df-ss 3447
This theorem is referenced by:  opabbrex  6338  opabbrexOLD  6339  opabex2  6736  soex  6741  fex2  6753  fnwelem  6913  fnse  6915  extmptsuppeq  6941  f1imaen2g  7628  ordtypelem10  8033  oismo  8046  wofib  8051  wemapso  8057  wdom2d  8086  wdomd  8087  unxpwdom2  8094  cantnfle  8166  cantnflt  8167  cantnflt2  8168  cantnfp1lem2  8174  cantnfp1lem3  8175  cantnflem1b  8181  cantnflem1d  8183  cantnflem1  8184  cnfcomlem  8194  cnfcom  8195  cnfcom2lem  8196  cnfcom3lem  8198  acni2  8466  fin1a2lem12  8830  hsmexlem1  8845  zorn2lem4  8918  fpwwe2lem2  9046  fpwwe2lem5  9048  fpwwe2lem12  9055  fpwwe2  9057  fpwwelem  9059  canthwelem  9064  pwfseqlem4  9076  trclfv  13032  hashbcss  14908  strssd  15111  restid2  15281  divsfval  15397  mrieqv2d  15489  mrissmrcd  15490  mreexexlemd  15494  mreexexlem3d  15496  mreexexlem4d  15497  mreexexd  15498  mreexdomd  15499  rescabs  15682  rescabs2  15683  resssetc  15931  resscatc  15944  estrres  15968  yonedalem1  16101  yonedalem21  16102  yonedalem3a  16103  yonedalem4c  16106  yonedalem22  16107  yonedalem3b  16108  yonedainv  16110  yonffthlem  16111  joinfval  16191  meetfval  16205  acsdomd  16371  gass  16899  pmtrfconj  17051  sylow2blem2  17201  dprdres  17589  dmdprdsplitlem  17598  pwssplit0  18209  pwssplit1  18210  pwssplit2  18211  pwssplit3  18212  opsrtoslem2  18636  evls1gsumadd  18841  evls1gsummul  18842  evl1gsummul  18876  frlmsplit2  19255  frlmsslss  19256  neiptoptop  20071  lpval  20079  neitr  20120  ordtbaslem  20128  ordtrest2  20144  cnrest2  20226  cnpresti  20228  cnprest  20229  cnprest2  20230  consuba  20359  consubclo  20363  uncon  20368  1stcelcls  20400  hausmapdom  20439  dissnref  20467  ptbasfi  20520  ptcls  20555  cnmpt2res  20616  qtopval2  20635  elqtop  20636  qtoprest  20656  ptuncnv  20746  ptunhmeo  20747  fsubbas  20806  elfm  20886  rnelfmlem  20891  rnelfm  20892  fmfnfmlem4  20896  flimclslem  20923  hauspwpwdom  20927  ptcmplem1  20991  cnextcn  21006  cnextfres1  21007  isust  21142  ustssel  21144  trust  21168  elutop  21172  restutop  21176  trcfilu  21233  cfiluweak  21234  psmetres2  21254  xmetres2  21300  fmcfil  22128  dvnf  22755  dvnbss  22756  dvaddf  22770  dvmulf  22771  dvcmulf  22773  dvcof  22776  ulmss  23214  perpln1  24609  perpln2  24610  isperp  24611  wlks  25089  trls  25108  sselpwd  27988  resf1o  28155  crefi  28510  ordtrest2NEW  28565  lmlim  28589  esummono  28711  esumrnmpt2  28725  esumpinfval  28730  carsgmon  28972  carsggect  28976  bnj1413  29629  cvmliftmolem1  29789  fwddifval  30711  neibastop1  30797  neibastop2lem  30798  fnejoin1  30806  filnetlem3  30818  filnetlem4  30819  dissneqlem  31473  elrfi  35245  elrfirn2  35247  relexpss1d  35940  wessf1ornlem  37086  limsupre  37297  limsupreOLD  37298  icccncfext  37341  dvdivcncf  37375  dvnprodlem1  37394  dvnprodlem2  37395  stoweidlem31  37465  stoweidlem53  37487  stoweidlem57  37491  stoweidlem59  37493  etransclem46  37716  saliuncl  37734  fsumlesge0  37757  sge0f1o  37762  sge0iunmptlemfi  37793  sge0iunmptlemre  37795  meadjuni  37808  meadjiunlem  37816  omessle  37832  omecl  37837
  Copyright terms: Public domain W3C validator