Theorem ssexd 4599

Description: A subclass of a set is a set. Deduction form of ssexg 4598. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
ssexd.1
ssexd.2

Assertion

Ref	Expression
ssexd

Proof of Theorem ssexd

Step	Hyp	Ref	Expression
1		ssexd.2	. 2
2		ssexd.1	. 2
3		ssexg 4598	. 2
4	1, 2, 3	syl2anc 661	1

Syntax hints:  ->wi 4  e.wcel 1818  cvv 3109  C_wss 3475

This theorem is referenced by:  opabbrex  6339  opabbrexOLD  6340  opabex2  6738  soex  6743  fex2  6755  fnwelem  6915  fnse  6917  extmptsuppeq  6943  f1imaen2g  7596  ordtypelem10  7973  oismo  7986  wofib  7991  wemapso  7997  wdom2d  8027  wdomd  8028  unxpwdom2  8035  cantnfle  8111  cantnflt  8112  cantnflt2  8113  cantnfp1lem2  8119  cantnfp1lem3  8120  cantnflem1b  8126  cantnflem1d  8128  cantnflem1  8129  cantnfleOLD  8141  cantnfltOLD  8142  cantnflt2OLD  8143  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1bOLD  8149  cantnflem1dOLD  8151  cantnflem1OLD  8152  cnfcomlem  8164  cnfcom  8165  cnfcom2lem  8166  cnfcom3lem  8168  cnfcomlemOLD  8172  cnfcomOLD  8173  cnfcom2lemOLD  8174  cnfcom3lemOLD  8176  acni2  8448  fin1a2lem12  8812  hsmexlem1  8827  zorn2lem4  8900  fpwwe2lem2  9031  fpwwe2lem5  9033  fpwwe2lem12  9040  fpwwe2  9042  fpwwelem  9044  canthwelem  9049  pwfseqlem4  9061  hashbcss  14522  strssd  14668  restid2  14828  divsfval  14944  mrieqv2d  15036  mrissmrcd  15037  mreexexlemd  15041  mreexexlem3d  15043  mreexexlem4d  15044  mreexexd  15045  mreexdomd  15046  rescabs  15202  rescabs2  15203  resssetc  15419  resscatc  15432  yonedalem1  15541  yonedalem21  15542  yonedalem3a  15543  yonedalem4c  15546  yonedalem22  15547  yonedalem3b  15548  yonedainv  15550  yonffthlem  15551  joinfval  15631  meetfval  15645  acsdomd  15811  gass  16339  pmtrfconj  16491  sylow2blem2  16641  dprdres  17075  dmdprdsplitlem  17084  pwssplit0  17704  pwssplit1  17705  pwssplit2  17706  pwssplit3  17707  mplsubglemOLD  18095  mpllsslemOLD  18096  opsrtoslem2  18149  evls1gsumadd  18361  evls1gsummul  18362  evl1gsummul  18396  frlmsplit2  18803  frlmsslss  18804  neiptoptop  19632  lpval  19640  neitr  19681  ordtbaslem  19689  ordtrest2  19705  cnrest2  19787  cnpresti  19789  cnprest  19790  cnprest2  19791  consuba  19921  consubclo  19925  uncon  19930  1stcelcls  19962  hausmapdom  20001  dissnref  20029  ptbasfi  20082  ptcls  20117  cnmpt2res  20178  qtopval2  20197  elqtop  20198  qtoprest  20218  ptuncnv  20308  ptunhmeo  20309  fsubbas  20368  elfm  20448  rnelfmlem  20453  rnelfm  20454  fmfnfmlem4  20458  flimclslem  20485  hauspwpwdom  20489  ptcmplem1  20552  cnextcn  20567  cnextfres  20568  isust  20706  ustssel  20708  trust  20732  elutop  20736  restutop  20740  trcfilu  20797  cfiluweak  20798  psmetres2  20818  xmetres2  20864  fmcfil  21711  dvnf  22330  dvnbss  22331  dvaddf  22345  dvmulf  22346  dvcmulf  22348  dvcof  22351  ulmss  22792  perpln1  24087  perpln2  24088  isperp  24089  wlks  24519  trls  24538  resf1o  27553  crefi  27850  ordtrest2NEW  27905  lmlim  27929  esummono  28066  esumpinfval  28079  omsfval  28265  cvmliftmolem1  28726  neibastop1  30177  neibastop2lem  30178  fnejoin1  30186  filnetlem3  30198  filnetlem4  30199  elrfi  30626  elrfirn2  30628  limsupre  31647  icccncfext  31690  dvdivcncf  31724  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem31  31813  stoweidlem53  31835  stoweidlem57  31839  stoweidlem59  31841  etransclem46  32063  estrres  32645  bnj1413  34091

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  ax-sep 4573

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-nfc 2607  df-v 3111  df-in 3482  df-ss 3489