Theorem ssexd 5268

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900

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 2707  ax-sep 5240

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 2714  df-cleq 2727  df-clel 2810  df-rab 3399  df-v 3441  df-in 3907  df-ss 3917

This theorem is referenced by:  abexd  5269  sselpwd  5272  moabex  5405  opabbrex  7411  soex  7863  fex2  7878  fabexd  7879  mapex  7883  funexw  7896  opabex2  8001  fnwelem  8073  fnse  8075  extmptsuppeq  8130  f1setex  8796  f1imaen2g  8954  fsuppss  9288  ordtypelem10  9434  oismo  9447  wofib  9452  wdom2d  9487  wdomd  9488  unxpwdom2  9495  ttrclexg  9634  djuexALT  9836  acni2  9958  fin1a2lem12  10323  hsmexlem1  10338  zorn2lem4  10411  ondomon  10475  fpwwe2lem2  10545  fpwwe2lem4  10547  fpwwe2lem11  10554  fpwwe2  10556  fpwwelem  10558  canthwelem  10563  pwfseqlem4  10575  hashf1lem1  14380  trclfv  14925  hashbcss  16934  strssd  17134  restid2  17352  divsfval  17470  mrieqv2d  17564  mrissmrcd  17565  mreexexlemd  17569  mreexexlem3d  17571  mreexexlem4d  17572  mreexdomd  17574  rescabs  17759  rescabs2  17760  resssetc  18018  resscatc  18035  estrres  18064  yonedalem1  18197  yonedalem21  18198  yonedalem3a  18199  yonedalem4c  18202  yonedalem22  18203  yonedalem3b  18204  yonedainv  18206  yonffthlem  18207  joinfval  18296  meetfval  18310  acsdomd  18482  ressmulgnnd  19010  gass  19232  pmtrfconj  19397  sylow2blem2  19552  dprdres  19961  dmdprdsplitlem  19970  primefld  20740  pwssplit0  21012  pwssplit1  21013  pwssplit2  21014  pwssplit3  21015  frlmsplit2  21730  frlmsslss  21731  opsrtoslem2  22013  evlsgsumadd  22053  evlsgsummul  22054  evls1gsumadd  22270  evls1gsummul  22271  evl1gsummul  22306  neiptoptop  23077  lpval  23085  neitr  23126  ordtbaslem  23134  ordtrest2  23150  cnrest2  23232  cnpresti  23234  cnprest  23235  cnprest2  23236  connsuba  23366  connsubclo  23370  unconn  23375  1stcelcls  23407  hausmapdom  23446  dissnref  23474  ptbasfi  23527  ptcls  23562  cnmpt2res  23623  qtopval2  23642  elqtop  23643  qtoprest  23663  ptuncnv  23753  ptunhmeo  23754  fsubbas  23813  elfm  23893  rnelfmlem  23898  rnelfm  23899  fmfnfmlem4  23903  flimclslem  23930  hauspwpwdom  23934  ptcmplem1  23998  cnextcn  24013  cnextfres1  24014  isust  24150  trust  24175  elutop  24179  restutop  24183  trcfilu  24239  cfiluweak  24240  psmetres2  24260  xmetres2  24307  fmcfil  25230  dvaddf  25903  dvmulf  25904  dvcmulf  25906  dvcof  25910  ulmss  26364  nosupno  27673  noinfno  27688  sssslt1  27771  sssslt2  27772  sltonex  28241  perpln1  28763  perpln2  28764  isperp  28765  wksfval  29664  fnpreimac  32728  fisuppov1  32741  resf1o  32788  hashpss  32868  gsumpart  33125  gsumwrd2dccat  33139  cycpmco2lem5  33191  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  erlval  33319  rlocval  33320  rlocbas  33328  fldgenval  33373  islinds5  33427  ellspds  33428  elrsp  33432  elrspunidl  33488  evlextv  33686  esplympl  33704  esplyind  33710  resssra  33722  lbslelsp  33733  lbsdiflsp0  33762  irngval  33821  ordtrest2NEW  34059  lmlim  34083  esummono  34190  esumrnmpt2  34204  esumpinfval  34209  elcarsg  34441  carsgmon  34450  carsggect  34454  reprval  34746  repr0  34747  reprsuc  34751  reprss  34753  reprinrn  34754  reprlt  34755  reprgt  34757  reprinfz1  34758  reprpmtf1o  34762  reprdifc  34763  bnj1413  35170  cvmliftmolem1  35454  satf0suclem  35548  fwddifval  36335  neibastop1  36532  neibastop2lem  36533  fnejoin1  36541  filnetlem3  36553  filnetlem4  36554  weiunse  36641  numiunnum  36643  bj-imdirval2lem  37356  bj-imdirval3  37358  bj-imdirco  37364  dissneqlem  37514  aks6d1c2lem4  42416  sticksstones20  42455  aks6d1c6lem3  42461  psrbagres  42836  selvcllemh  42860  selvcllem4  42861  selvcllem5  42862  selvcl  42863  selvval2  42864  selvvvval  42865  evlselv  42867  selvadd  42868  selvmul  42869  fsuppssindlem2  42872  fsuppssind  42873  elrfi  42973  elrfirn2  42975  oaun3lem3  43655  nadd2rabex  43665  clcnvlem  43901  relexpss1d  43983  k0004lem2  44426  ixpssmapc  45355  restuni4  45402  restsubel  45434  wessf1ornlem  45466  disjinfi  45473  unirnmap  45489  inmap  45490  difmapsn  45493  unirnmapsn  45495  ssmapsn  45497  limsupre  45922  limsuppnfdlem  45982  limsuppnflem  45991  limsupmnflem  46001  limsupre2lem  46005  liminfval4  46070  liminfval3  46071  icccncfext  46168  dvdivcncf  46208  dvnprodlem1  46227  dvnprodlem2  46228  ovolsplit  46269  stoweidlem31  46312  stoweidlem53  46334  stoweidlem57  46338  stoweidlem59  46340  etransclem46  46561  salexct  46615  subsaluni  46641  fsumlesge0  46658  sge0iunmptlemfi  46694  sge0iunmptlemre  46696  meadjuni  46738  meadjiunlem  46746  omessle  46779  omecl  46784  isomenndlem  46811  caragencmpl  46816  ovnval2  46826  ovnval2b  46833  ovncvrrp  46845  ovncl  46848  hoidmvlelem2  46877  hoidmvlelem3  46878  ovncvr2  46892  ovnsubadd2lem  46926  ovnovollem3  46939  vonvolmbllem  46941  vonvolmbl  46942  sssmf  47019  incsmf  47023  issmflelem  47025  issmfle  47026  smfconst  47030  issmfgtlem  47036  issmfgt  47037  smfaddlem2  47045  decsmf  47048  issmfgelem  47050  issmfge  47051  nsssmfmbflem  47059  smfpimioo  47068  smfresal  47069  smfmullem4  47075  smfpimbor1lem1  47079  smf2id  47082  upwlksfval  48418  toplatglb  49283