Theorem ssexd 5324

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

Hypotheses

Ref	Expression
ssexd.1	⊢ (𝜑 → 𝐵 ∈ 𝐶)
ssexd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem ssexd

Step	Hyp	Ref	Expression
1		ssexd.2	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssexd.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		ssexg 5323	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 584	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  abexd  5325  sselpwd  5328  opabbrex  7484  soex  7943  fex2  7958  fabexd  7959  mapex  7963  funexw  7976  opabex2  8082  fnwelem  8156  fnse  8158  extmptsuppeq  8213  f1setex  8897  f1imaen2g  9055  fsuppss  9423  ordtypelem10  9567  oismo  9580  wofib  9585  wdom2d  9620  wdomd  9621  unxpwdom2  9628  ttrclexg  9763  djuexALT  9962  acni2  10086  fin1a2lem12  10451  hsmexlem1  10466  zorn2lem4  10539  fpwwe2lem2  10672  fpwwe2lem4  10674  fpwwe2lem11  10681  fpwwe2  10683  fpwwelem  10685  canthwelem  10690  pwfseqlem4  10702  hashf1lem1  14494  trclfv  15039  hashbcss  17042  strssd  17242  restid2  17475  divsfval  17592  mrieqv2d  17682  mrissmrcd  17683  mreexexlemd  17687  mreexexlem3d  17689  mreexexlem4d  17690  mreexdomd  17692  rescabs  17877  rescabsOLD  17878  rescabs2  17879  resssetc  18137  resscatc  18154  estrres  18184  yonedalem1  18317  yonedalem21  18318  yonedalem3a  18319  yonedalem4c  18322  yonedalem22  18323  yonedalem3b  18324  yonedainv  18326  yonffthlem  18327  joinfval  18418  meetfval  18432  acsdomd  18602  ressmulgnnd  19096  gass  19319  pmtrfconj  19484  sylow2blem2  19639  dprdres  20048  dmdprdsplitlem  20057  primefld  20806  pwssplit0  21057  pwssplit1  21058  pwssplit2  21059  pwssplit3  21060  frlmsplit2  21793  frlmsslss  21794  opsrtoslem2  22080  evlsgsumadd  22115  evlsgsummul  22116  evls1gsumadd  22328  evls1gsummul  22329  evl1gsummul  22364  neiptoptop  23139  lpval  23147  neitr  23188  ordtbaslem  23196  ordtrest2  23212  cnrest2  23294  cnpresti  23296  cnprest  23297  cnprest2  23298  connsuba  23428  connsubclo  23432  unconn  23437  1stcelcls  23469  hausmapdom  23508  dissnref  23536  ptbasfi  23589  ptcls  23624  cnmpt2res  23685  qtopval2  23704  elqtop  23705  qtoprest  23725  ptuncnv  23815  ptunhmeo  23816  fsubbas  23875  elfm  23955  rnelfmlem  23960  rnelfm  23961  fmfnfmlem4  23965  flimclslem  23992  hauspwpwdom  23996  ptcmplem1  24060  cnextcn  24075  cnextfres1  24076  isust  24212  trust  24238  elutop  24242  restutop  24246  trcfilu  24303  cfiluweak  24304  psmetres2  24324  xmetres2  24371  fmcfil  25306  dvaddf  25979  dvmulf  25980  dvcmulf  25982  dvcof  25986  ulmss  26440  nosupno  27748  noinfno  27763  sssslt1  27840  sssslt2  27841  sltonex  28284  perpln1  28718  perpln2  28719  isperp  28720  wksfval  29627  fnpreimac  32681  fisuppov1  32692  resf1o  32741  hashpss  32813  gsumpart  33060  gsumwrd2dccat  33070  cycpmco2lem5  33150  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspn  33250  erlval  33262  rlocval  33263  rlocbas  33271  fldgenval  33314  islinds5  33395  ellspds  33396  elrsp  33400  elrspunidl  33456  resssra  33638  lbslelsp  33648  lbsdiflsp0  33677  irngval  33735  ordtrest2NEW  33922  lmlim  33946  esummono  34055  esumrnmpt2  34069  esumpinfval  34074  elcarsg  34307  carsgmon  34316  carsggect  34320  reprval  34625  repr0  34626  reprsuc  34630  reprss  34632  reprinrn  34633  reprlt  34634  reprgt  34636  reprinfz1  34637  reprpmtf1o  34641  reprdifc  34642  bnj1413  35049  cvmliftmolem1  35286  satf0suclem  35380  fwddifval  36163  neibastop1  36360  neibastop2lem  36361  fnejoin1  36369  filnetlem3  36381  filnetlem4  36382  weiunse  36469  numiunnum  36471  bj-imdirval2lem  37183  bj-imdirval3  37185  bj-imdirco  37191  dissneqlem  37341  aks6d1c2lem4  42128  sticksstones20  42167  aks6d1c6lem3  42173  psrbagres  42556  selvcllemh  42590  selvcllem4  42591  selvcllem5  42592  selvcl  42593  selvval2  42594  selvvvval  42595  evlselv  42597  selvadd  42598  selvmul  42599  fsuppssindlem2  42602  fsuppssind  42603  elrfi  42705  elrfirn2  42707  oaun3lem3  43389  nadd2rabex  43399  clcnvlem  43636  relexpss1d  43718  k0004lem2  44161  ixpssmapc  45078  restuni4  45126  restsubel  45158  wessf1ornlem  45190  disjinfi  45197  unirnmap  45213  inmap  45214  difmapsn  45217  unirnmapsn  45219  ssmapsn  45221  limsupre  45656  limsuppnfdlem  45716  limsuppnflem  45725  limsupmnflem  45735  limsupre2lem  45739  liminfval4  45804  liminfval3  45805  icccncfext  45902  dvdivcncf  45942  dvnprodlem1  45961  dvnprodlem2  45962  ovolsplit  46003  stoweidlem31  46046  stoweidlem53  46068  stoweidlem57  46072  stoweidlem59  46074  etransclem46  46295  salexct  46349  subsaluni  46375  fsumlesge0  46392  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  meadjuni  46472  meadjiunlem  46480  omessle  46513  omecl  46518  isomenndlem  46545  caragencmpl  46550  ovnval2  46560  ovnval2b  46567  ovncvrrp  46579  ovncl  46582  hoidmvlelem2  46611  hoidmvlelem3  46612  ovncvr2  46626  ovnsubadd2lem  46660  ovnovollem3  46673  vonvolmbllem  46675  vonvolmbl  46676  sssmf  46753  incsmf  46757  issmflelem  46759  issmfle  46760  smfconst  46764  issmfgtlem  46770  issmfgt  46771  smfaddlem2  46779  decsmf  46782  issmfgelem  46784  issmfge  46785  nsssmfmbflem  46793  smfpimioo  46802  smfresal  46803  smfmullem4  46809  smfpimbor1lem1  46813  smf2id  46816  upwlksfval  48051  toplatglb  48890