Theorem ssexd 5262

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890

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 5232

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 3391  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  abexd  5263  sselpwd  5266  moabex  5407  opabbrex  7415  soex  7867  fex2  7882  fabexd  7883  mapex  7887  funexw  7900  opabex2  8005  fnwelem  8076  fnse  8078  extmptsuppeq  8133  f1setex  8799  f1imaen2g  8957  fsuppss  9291  ordtypelem10  9437  oismo  9450  wofib  9455  wdom2d  9490  wdomd  9491  unxpwdom2  9498  ttrclexg  9639  djuexALT  9841  acni2  9963  fin1a2lem12  10328  hsmexlem1  10343  zorn2lem4  10416  ondomon  10480  fpwwe2lem2  10550  fpwwe2lem4  10552  fpwwe2lem11  10559  fpwwe2  10561  fpwwelem  10563  canthwelem  10568  pwfseqlem4  10580  hashf1lem1  14412  trclfv  14957  hashbcss  16970  strssd  17170  restid2  17388  divsfval  17506  mrieqv2d  17600  mrissmrcd  17601  mreexexlemd  17605  mreexexlem3d  17607  mreexexlem4d  17608  mreexdomd  17610  rescabs  17795  rescabs2  17796  resssetc  18054  resscatc  18071  estrres  18100  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedainv  18242  yonffthlem  18243  joinfval  18332  meetfval  18346  acsdomd  18518  ressmulgnnd  19049  gass  19271  pmtrfconj  19436  sylow2blem2  19591  dprdres  20000  dmdprdsplitlem  20009  primefld  20777  pwssplit0  21049  pwssplit1  21050  pwssplit2  21051  pwssplit3  21052  frlmsplit2  21767  frlmsslss  21768  opsrtoslem2  22048  evlsgsumadd  22088  evlsgsummul  22089  evls1gsumadd  22303  evls1gsummul  22304  evl1gsummul  22339  neiptoptop  23110  lpval  23118  neitr  23159  ordtbaslem  23167  ordtrest2  23183  cnrest2  23265  cnpresti  23267  cnprest  23268  cnprest2  23269  connsuba  23399  connsubclo  23403  unconn  23408  1stcelcls  23440  hausmapdom  23479  dissnref  23507  ptbasfi  23560  ptcls  23595  cnmpt2res  23656  qtopval2  23675  elqtop  23676  qtoprest  23696  ptuncnv  23786  ptunhmeo  23787  fsubbas  23846  elfm  23926  rnelfmlem  23931  rnelfm  23932  fmfnfmlem4  23936  flimclslem  23963  hauspwpwdom  23967  ptcmplem1  24031  cnextcn  24046  cnextfres1  24047  isust  24183  trust  24208  elutop  24212  restutop  24216  trcfilu  24272  cfiluweak  24273  psmetres2  24293  xmetres2  24340  fmcfil  25253  dvaddf  25923  dvmulf  25924  dvcmulf  25926  dvcof  25929  ulmss  26379  nosupno  27685  noinfno  27700  ssslts1  27783  ssslts2  27784  ltonsex  28272  perpln1  28796  perpln2  28797  isperp  28798  wksfval  29697  fnpreimac  32762  fisuppov1  32775  resf1o  32822  hashpss  32901  gsumpart  33143  gsumwrd2dccat  33158  cycpmco2lem5  33210  elrgspnlem1  33322  elrgspnlem2  33323  elrgspnlem3  33324  elrgspnlem4  33325  elrgspn  33326  erlval  33338  rlocval  33339  rlocbas  33347  fldgenval  33392  islinds5  33446  ellspds  33447  elrsp  33451  elrspunidl  33507  evlextv  33705  psrmonprod  33715  esplympl  33730  esplyind  33738  resssra  33750  lbslelsp  33761  lbsdiflsp0  33790  irngval  33849  ordtrest2NEW  34087  lmlim  34111  esummono  34218  esumrnmpt2  34232  esumpinfval  34237  elcarsg  34469  carsgmon  34478  carsggect  34482  reprval  34774  repr0  34775  reprsuc  34779  reprss  34781  reprinrn  34782  reprlt  34783  reprgt  34785  reprinfz1  34786  reprpmtf1o  34790  reprdifc  34791  bnj1413  35197  cvmliftmolem1  35483  satf0suclem  35577  fwddifval  36364  neibastop1  36561  neibastop2lem  36562  fnejoin1  36570  filnetlem3  36582  filnetlem4  36583  weiunse  36670  numiunnum  36672  bj-imdirval2lem  37516  bj-imdirval3  37518  bj-imdirco  37524  dissneqlem  37676  aks6d1c2lem4  42586  sticksstones20  42625  aks6d1c6lem3  42631  psrbagres  43009  selvcllemh  43033  selvcllem4  43034  selvcllem5  43035  selvcl  43036  selvval2  43037  selvvvval  43038  evlselv  43040  selvadd  43041  selvmul  43042  fsuppssindlem2  43045  fsuppssind  43046  elrfi  43146  elrfirn2  43148  oaun3lem3  43828  nadd2rabex  43838  clcnvlem  44074  relexpss1d  44156  k0004lem2  44599  ixpssmapc  45528  restuni4  45575  restsubel  45607  wessf1ornlem  45639  disjinfi  45646  unirnmap  45661  inmap  45662  difmapsn  45665  unirnmapsn  45667  ssmapsn  45669  limsupre  46093  limsuppnfdlem  46153  limsuppnflem  46162  limsupmnflem  46172  limsupre2lem  46176  liminfval4  46241  liminfval3  46242  icccncfext  46339  dvdivcncf  46379  dvnprodlem1  46398  dvnprodlem2  46399  ovolsplit  46440  stoweidlem31  46483  stoweidlem53  46505  stoweidlem57  46509  stoweidlem59  46511  etransclem46  46732  salexct  46786  subsaluni  46812  fsumlesge0  46829  sge0iunmptlemfi  46865  sge0iunmptlemre  46867  meadjuni  46909  meadjiunlem  46917  omessle  46950  omecl  46955  isomenndlem  46982  caragencmpl  46987  ovnval2  46997  ovnval2b  47004  ovncvrrp  47016  ovncl  47019  hoidmvlelem2  47048  hoidmvlelem3  47049  ovncvr2  47063  ovnsubadd2lem  47097  ovnovollem3  47110  vonvolmbllem  47112  vonvolmbl  47113  sssmf  47190  incsmf  47194  issmflelem  47196  issmfle  47197  smfconst  47201  issmfgtlem  47207  issmfgt  47208  smfaddlem2  47216  decsmf  47219  issmfgelem  47221  issmfge  47222  nsssmfmbflem  47230  smfpimioo  47239  smfresal  47240  smfmullem4  47246  smfpimbor1lem1  47250  smf2id  47253  upwlksfval  48629  toplatglb  49494