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

Theorem ssexd 4550
Description: A subclass of a set is a set. Deduction form of ssexg 4549. (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 4549 . 2  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   _Vcvv 3045    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418
This theorem is referenced by:  opabbrex  6332  opabbrexOLD  6333  opabex2  6731  soex  6736  fex2  6748  fnwelem  6911  fnse  6913  extmptsuppeq  6939  f1imaen2g  7630  ordtypelem10  8042  oismo  8055  wofib  8060  wemapso  8066  wdom2d  8095  wdomd  8096  unxpwdom2  8103  cantnfle  8176  cantnflt  8177  cantnflt2  8178  cantnfp1lem2  8184  cantnfp1lem3  8185  cantnflem1b  8191  cantnflem1d  8193  cantnflem1  8194  cnfcomlem  8204  cnfcom  8205  cnfcom2lem  8206  cnfcom3lem  8208  acni2  8477  fin1a2lem12  8841  hsmexlem1  8856  zorn2lem4  8929  fpwwe2lem2  9057  fpwwe2lem5  9059  fpwwe2lem12  9066  fpwwe2  9068  fpwwelem  9070  canthwelem  9075  pwfseqlem4  9087  trclfv  13064  hashbcss  14956  strssd  15159  restid2  15329  divsfval  15453  mrieqv2d  15545  mrissmrcd  15546  mreexexlemd  15550  mreexexlem3d  15552  mreexexlem4d  15553  mreexexd  15554  mreexdomd  15555  rescabs  15738  rescabs2  15739  resssetc  15987  resscatc  16000  estrres  16024  yonedalem1  16157  yonedalem21  16158  yonedalem3a  16159  yonedalem4c  16162  yonedalem22  16163  yonedalem3b  16164  yonedainv  16166  yonffthlem  16167  joinfval  16247  meetfval  16261  acsdomd  16427  gass  16955  pmtrfconj  17107  sylow2blem2  17273  dprdres  17661  dmdprdsplitlem  17670  pwssplit0  18281  pwssplit1  18282  pwssplit2  18283  pwssplit3  18284  opsrtoslem2  18708  evls1gsumadd  18913  evls1gsummul  18914  evl1gsummul  18948  frlmsplit2  19331  frlmsslss  19332  neiptoptop  20147  lpval  20155  neitr  20196  ordtbaslem  20204  ordtrest2  20220  cnrest2  20302  cnpresti  20304  cnprest  20305  cnprest2  20306  consuba  20435  consubclo  20439  uncon  20444  1stcelcls  20476  hausmapdom  20515  dissnref  20543  ptbasfi  20596  ptcls  20631  cnmpt2res  20692  qtopval2  20711  elqtop  20712  qtoprest  20732  ptuncnv  20822  ptunhmeo  20823  fsubbas  20882  elfm  20962  rnelfmlem  20967  rnelfm  20968  fmfnfmlem4  20972  flimclslem  20999  hauspwpwdom  21003  ptcmplem1  21067  cnextcn  21082  cnextfres1  21083  isust  21218  ustssel  21220  trust  21244  elutop  21248  restutop  21252  trcfilu  21309  cfiluweak  21310  psmetres2  21330  xmetres2  21376  fmcfil  22242  dvnf  22881  dvnbss  22882  dvaddf  22896  dvmulf  22897  dvcmulf  22899  dvcof  22902  ulmss  23352  perpln1  24755  perpln2  24756  isperp  24757  wlks  25247  trls  25266  sselpwd  28153  resf1o  28315  crefi  28674  ordtrest2NEW  28729  lmlim  28753  esummono  28875  esumrnmpt2  28889  esumpinfval  28894  carsgmon  29146  carsggect  29150  bnj1413  29844  cvmliftmolem1  30004  fwddifval  30929  neibastop1  31015  neibastop2lem  31016  fnejoin1  31024  filnetlem3  31036  filnetlem4  31037  dissneqlem  31742  elrfi  35536  elrfirn2  35538  clcnvlem  36230  relexpss1d  36297  ixpssmapc  37418  wessf1ornlem  37459  limsupre  37721  limsupreOLD  37722  icccncfext  37765  dvdivcncf  37799  dvnprodlem1  37821  dvnprodlem2  37822  stoweidlem31  37892  stoweidlem53  37914  stoweidlem57  37918  stoweidlem59  37920  etransclem46  38145  saliuncl  38183  salexct  38193  fsumlesge0  38219  sge0f1o  38224  sge0iunmptlemfi  38255  sge0iunmptlemre  38257  meadjuni  38295  meadjiunlem  38303  omessle  38319  omecl  38324  isomenndlem  38351  caragencmpl  38356  ovnval2  38367  ovnval2b  38374  ovncvrrp  38386  ovncl  38389  hoidmvlelem2  38418  hoidmvlelem3  38419  ovncvr2  38433  1wlksfval  39626  wlksfval  39627
  Copyright terms: Public domain W3C validator