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

Theorem ssexd 4543
Description: A subclass of a set is a set. Deduction form of ssexg 4542. (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 4542 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 673 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1904   _Vcvv 3031    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404
This theorem is referenced by:  sselpwd  4544  opabbrex  6350  opabex2  6750  soex  6755  fex2  6767  fnwelem  6930  fnse  6932  extmptsuppeq  6958  f1imaen2g  7648  ordtypelem10  8060  oismo  8073  wofib  8078  wemapso  8084  wdom2d  8113  wdomd  8114  unxpwdom2  8121  cantnfle  8194  cantnflt  8195  cantnflt2  8196  cantnfp1lem2  8202  cantnfp1lem3  8203  cantnflem1b  8209  cantnflem1d  8211  cantnflem1  8212  cnfcomlem  8222  cnfcom  8223  cnfcom2lem  8224  cnfcom3lem  8226  acni2  8495  fin1a2lem12  8859  hsmexlem1  8874  zorn2lem4  8947  fpwwe2lem2  9075  fpwwe2lem5  9077  fpwwe2lem12  9084  fpwwe2  9086  fpwwelem  9088  canthwelem  9093  pwfseqlem4  9105  trclfv  13141  hashbcss  15035  strssd  15237  restid2  15407  divsfval  15531  mrieqv2d  15623  mrissmrcd  15624  mreexexlemd  15628  mreexexlem3d  15630  mreexexlem4d  15631  mreexexd  15632  mreexdomd  15633  rescabs  15816  rescabs2  15817  resssetc  16065  resscatc  16078  estrres  16102  yonedalem1  16235  yonedalem21  16236  yonedalem3a  16237  yonedalem4c  16240  yonedalem22  16241  yonedalem3b  16242  yonedainv  16244  yonffthlem  16245  joinfval  16325  meetfval  16339  acsdomd  16505  gass  17033  pmtrfconj  17185  sylow2blem2  17351  dprdres  17739  dmdprdsplitlem  17748  pwssplit0  18359  pwssplit1  18360  pwssplit2  18361  pwssplit3  18362  opsrtoslem2  18785  evls1gsumadd  18990  evls1gsummul  18991  evl1gsummul  19025  frlmsplit2  19408  frlmsslss  19409  neiptoptop  20224  lpval  20232  neitr  20273  ordtbaslem  20281  ordtrest2  20297  cnrest2  20379  cnpresti  20381  cnprest  20382  cnprest2  20383  consuba  20512  consubclo  20516  uncon  20521  1stcelcls  20553  hausmapdom  20592  dissnref  20620  ptbasfi  20673  ptcls  20708  cnmpt2res  20769  qtopval2  20788  elqtop  20789  qtoprest  20809  ptuncnv  20899  ptunhmeo  20900  fsubbas  20960  elfm  21040  rnelfmlem  21045  rnelfm  21046  fmfnfmlem4  21050  flimclslem  21077  hauspwpwdom  21081  ptcmplem1  21145  cnextcn  21160  cnextfres1  21161  isust  21296  ustssel  21298  trust  21322  elutop  21326  restutop  21330  trcfilu  21387  cfiluweak  21388  psmetres2  21408  xmetres2  21454  fmcfil  22320  dvnf  22960  dvnbss  22961  dvaddf  22975  dvmulf  22976  dvcmulf  22978  dvcof  22981  ulmss  23431  perpln1  24834  perpln2  24835  isperp  24836  wlks  25326  trls  25345  resf1o  28390  crefi  28748  ordtrest2NEW  28803  lmlim  28827  esummono  28949  esumrnmpt2  28963  esumpinfval  28968  carsgmon  29219  carsggect  29223  bnj1413  29916  cvmliftmolem1  30076  fwddifval  31000  neibastop1  31086  neibastop2lem  31087  fnejoin1  31095  filnetlem3  31107  filnetlem4  31108  dissneqlem  31812  elrfi  35607  elrfirn2  35609  clcnvlem  36301  relexpss1d  36368  ixpssmapc  37477  wessf1ornlem  37530  unirnmap  37560  inmap  37562  difmapsn  37565  unirnmapsn  37567  ssmapsn  37569  limsupre  37818  limsupreOLD  37819  icccncfext  37862  dvdivcncf  37896  dvnprodlem1  37918  dvnprodlem2  37919  ovolsplit  37963  stoweidlem31  38004  stoweidlem53  38026  stoweidlem57  38030  stoweidlem59  38032  etransclem46  38257  saliuncl  38295  salexct  38305  fsumlesge0  38333  sge0f1o  38338  sge0iunmptlemfi  38369  sge0iunmptlemre  38371  meadjuni  38411  meadjiunlem  38419  omessle  38438  omecl  38443  isomenndlem  38470  caragencmpl  38475  ovnval2  38485  ovnval2b  38492  ovncvrrp  38504  ovncl  38507  hoidmvlelem2  38536  hoidmvlelem3  38537  ovncvr2  38551  ovnsubadd2lem  38585  ovnovollem3  38598  vonvolmbllem  38600  vonvolmbl  38601  1wlksfval  39813  wlksfval  39814
  Copyright terms: Public domain W3C validator