Theorem ssexd 5273

Description: A subclass of a set is a set. Deduction form of ssexg 5272. (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 5272	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  abexd  5274  sselpwd  5277  moabex  5415  opabbrex  7423  soex  7875  fex2  7890  fabexd  7891  mapex  7895  funexw  7908  opabex2  8013  fnwelem  8085  fnse  8087  extmptsuppeq  8142  f1setex  8808  f1imaen2g  8966  fsuppss  9300  ordtypelem10  9446  oismo  9459  wofib  9464  wdom2d  9499  wdomd  9500  unxpwdom2  9507  ttrclexg  9646  djuexALT  9848  acni2  9970  fin1a2lem12  10335  hsmexlem1  10350  zorn2lem4  10423  ondomon  10487  fpwwe2lem2  10557  fpwwe2lem4  10559  fpwwe2lem11  10566  fpwwe2  10568  fpwwelem  10570  canthwelem  10575  pwfseqlem4  10587  hashf1lem1  14392  trclfv  14937  hashbcss  16946  strssd  17146  restid2  17364  divsfval  17482  mrieqv2d  17576  mrissmrcd  17577  mreexexlemd  17581  mreexexlem3d  17583  mreexexlem4d  17584  mreexdomd  17586  rescabs  17771  rescabs2  17772  resssetc  18030  resscatc  18047  estrres  18076  yonedalem1  18209  yonedalem21  18210  yonedalem3a  18211  yonedalem4c  18214  yonedalem22  18215  yonedalem3b  18216  yonedainv  18218  yonffthlem  18219  joinfval  18308  meetfval  18322  acsdomd  18494  ressmulgnnd  19025  gass  19247  pmtrfconj  19412  sylow2blem2  19567  dprdres  19976  dmdprdsplitlem  19985  primefld  20755  pwssplit0  21027  pwssplit1  21028  pwssplit2  21029  pwssplit3  21030  frlmsplit2  21745  frlmsslss  21746  opsrtoslem2  22028  evlsgsumadd  22068  evlsgsummul  22069  evls1gsumadd  22285  evls1gsummul  22286  evl1gsummul  22321  neiptoptop  23092  lpval  23100  neitr  23141  ordtbaslem  23149  ordtrest2  23165  cnrest2  23247  cnpresti  23249  cnprest  23250  cnprest2  23251  connsuba  23381  connsubclo  23385  unconn  23390  1stcelcls  23422  hausmapdom  23461  dissnref  23489  ptbasfi  23542  ptcls  23577  cnmpt2res  23638  qtopval2  23657  elqtop  23658  qtoprest  23678  ptuncnv  23768  ptunhmeo  23769  fsubbas  23828  elfm  23908  rnelfmlem  23913  rnelfm  23914  fmfnfmlem4  23918  flimclslem  23945  hauspwpwdom  23949  ptcmplem1  24013  cnextcn  24028  cnextfres1  24029  isust  24165  trust  24190  elutop  24194  restutop  24198  trcfilu  24254  cfiluweak  24255  psmetres2  24275  xmetres2  24322  fmcfil  25245  dvaddf  25918  dvmulf  25919  dvcmulf  25921  dvcof  25925  ulmss  26379  nosupno  27688  noinfno  27703  ssslts1  27786  ssslts2  27787  ltonsex  28275  perpln1  28800  perpln2  28801  isperp  28802  wksfval  29701  fnpreimac  32766  fisuppov1  32779  resf1o  32826  hashpss  32906  gsumpart  33163  gsumwrd2dccat  33178  cycpmco2lem5  33230  elrgspnlem1  33342  elrgspnlem2  33343  elrgspnlem3  33344  elrgspnlem4  33345  elrgspn  33346  erlval  33358  rlocval  33359  rlocbas  33367  fldgenval  33412  islinds5  33466  ellspds  33467  elrsp  33471  elrspunidl  33527  evlextv  33725  psrmonprod  33735  esplympl  33750  esplyind  33758  resssra  33770  lbslelsp  33781  lbsdiflsp0  33810  irngval  33869  ordtrest2NEW  34107  lmlim  34131  esummono  34238  esumrnmpt2  34252  esumpinfval  34257  elcarsg  34489  carsgmon  34498  carsggect  34502  reprval  34794  repr0  34795  reprsuc  34799  reprss  34801  reprinrn  34802  reprlt  34803  reprgt  34805  reprinfz1  34806  reprpmtf1o  34810  reprdifc  34811  bnj1413  35217  cvmliftmolem1  35503  satf0suclem  35597  fwddifval  36384  neibastop1  36581  neibastop2lem  36582  fnejoin1  36590  filnetlem3  36602  filnetlem4  36603  weiunse  36690  numiunnum  36692  bj-imdirval2lem  37464  bj-imdirval3  37466  bj-imdirco  37472  dissneqlem  37622  aks6d1c2lem4  42526  sticksstones20  42565  aks6d1c6lem3  42571  psrbagres  42943  selvcllemh  42967  selvcllem4  42968  selvcllem5  42969  selvcl  42970  selvval2  42971  selvvvval  42972  evlselv  42974  selvadd  42975  selvmul  42976  fsuppssindlem2  42979  fsuppssind  42980  elrfi  43080  elrfirn2  43082  oaun3lem3  43762  nadd2rabex  43772  clcnvlem  44008  relexpss1d  44090  k0004lem2  44533  ixpssmapc  45462  restuni4  45509  restsubel  45541  wessf1ornlem  45573  disjinfi  45580  unirnmap  45595  inmap  45596  difmapsn  45599  unirnmapsn  45601  ssmapsn  45603  limsupre  46028  limsuppnfdlem  46088  limsuppnflem  46097  limsupmnflem  46107  limsupre2lem  46111  liminfval4  46176  liminfval3  46177  icccncfext  46274  dvdivcncf  46314  dvnprodlem1  46333  dvnprodlem2  46334  ovolsplit  46375  stoweidlem31  46418  stoweidlem53  46440  stoweidlem57  46444  stoweidlem59  46446  etransclem46  46667  salexct  46721  subsaluni  46747  fsumlesge0  46764  sge0iunmptlemfi  46800  sge0iunmptlemre  46802  meadjuni  46844  meadjiunlem  46852  omessle  46885  omecl  46890  isomenndlem  46917  caragencmpl  46922  ovnval2  46932  ovnval2b  46939  ovncvrrp  46951  ovncl  46954  hoidmvlelem2  46983  hoidmvlelem3  46984  ovncvr2  46998  ovnsubadd2lem  47032  ovnovollem3  47045  vonvolmbllem  47047  vonvolmbl  47048  sssmf  47125  incsmf  47129  issmflelem  47131  issmfle  47132  smfconst  47136  issmfgtlem  47142  issmfgt  47143  smfaddlem2  47151  decsmf  47154  issmfgelem  47156  issmfge  47157  nsssmfmbflem  47165  smfpimioo  47174  smfresal  47175  smfmullem4  47181  smfpimbor1lem1  47185  smf2id  47188  upwlksfval  48524  toplatglb  49389