Theorem ssexd 5270

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902

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 5242

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 3401  df-v 3443  df-in 3909  df-ss 3919

This theorem is referenced by:  abexd  5271  sselpwd  5274  moabex  5407  opabbrex  7413  soex  7865  fex2  7880  fabexd  7881  mapex  7885  funexw  7898  opabex2  8003  fnwelem  8075  fnse  8077  extmptsuppeq  8132  f1setex  8798  f1imaen2g  8956  fsuppss  9290  ordtypelem10  9436  oismo  9449  wofib  9454  wdom2d  9489  wdomd  9490  unxpwdom2  9497  ttrclexg  9636  djuexALT  9838  acni2  9960  fin1a2lem12  10325  hsmexlem1  10340  zorn2lem4  10413  ondomon  10477  fpwwe2lem2  10547  fpwwe2lem4  10549  fpwwe2lem11  10556  fpwwe2  10558  fpwwelem  10560  canthwelem  10565  pwfseqlem4  10577  hashf1lem1  14382  trclfv  14927  hashbcss  16936  strssd  17136  restid2  17354  divsfval  17472  mrieqv2d  17566  mrissmrcd  17567  mreexexlemd  17571  mreexexlem3d  17573  mreexexlem4d  17574  mreexdomd  17576  rescabs  17761  rescabs2  17762  resssetc  18020  resscatc  18037  estrres  18066  yonedalem1  18199  yonedalem21  18200  yonedalem3a  18201  yonedalem4c  18204  yonedalem22  18205  yonedalem3b  18206  yonedainv  18208  yonffthlem  18209  joinfval  18298  meetfval  18312  acsdomd  18484  ressmulgnnd  19012  gass  19234  pmtrfconj  19399  sylow2blem2  19554  dprdres  19963  dmdprdsplitlem  19972  primefld  20742  pwssplit0  21014  pwssplit1  21015  pwssplit2  21016  pwssplit3  21017  frlmsplit2  21732  frlmsslss  21733  opsrtoslem2  22015  evlsgsumadd  22055  evlsgsummul  22056  evls1gsumadd  22272  evls1gsummul  22273  evl1gsummul  22308  neiptoptop  23079  lpval  23087  neitr  23128  ordtbaslem  23136  ordtrest2  23152  cnrest2  23234  cnpresti  23236  cnprest  23237  cnprest2  23238  connsuba  23368  connsubclo  23372  unconn  23377  1stcelcls  23409  hausmapdom  23448  dissnref  23476  ptbasfi  23529  ptcls  23564  cnmpt2res  23625  qtopval2  23644  elqtop  23645  qtoprest  23665  ptuncnv  23755  ptunhmeo  23756  fsubbas  23815  elfm  23895  rnelfmlem  23900  rnelfm  23901  fmfnfmlem4  23905  flimclslem  23932  hauspwpwdom  23936  ptcmplem1  24000  cnextcn  24015  cnextfres1  24016  isust  24152  trust  24177  elutop  24181  restutop  24185  trcfilu  24241  cfiluweak  24242  psmetres2  24262  xmetres2  24309  fmcfil  25232  dvaddf  25905  dvmulf  25906  dvcmulf  25908  dvcof  25912  ulmss  26366  nosupno  27675  noinfno  27690  ssslts1  27773  ssslts2  27774  ltonsex  28262  perpln1  28786  perpln2  28787  isperp  28788  wksfval  29687  fnpreimac  32751  fisuppov1  32764  resf1o  32811  hashpss  32891  gsumpart  33148  gsumwrd2dccat  33162  cycpmco2lem5  33214  elrgspnlem1  33326  elrgspnlem2  33327  elrgspnlem3  33328  elrgspnlem4  33329  elrgspn  33330  erlval  33342  rlocval  33343  rlocbas  33351  fldgenval  33396  islinds5  33450  ellspds  33451  elrsp  33455  elrspunidl  33511  evlextv  33709  esplympl  33727  esplyind  33733  resssra  33745  lbslelsp  33756  lbsdiflsp0  33785  irngval  33844  ordtrest2NEW  34082  lmlim  34106  esummono  34213  esumrnmpt2  34227  esumpinfval  34232  elcarsg  34464  carsgmon  34473  carsggect  34477  reprval  34769  repr0  34770  reprsuc  34774  reprss  34776  reprinrn  34777  reprlt  34778  reprgt  34780  reprinfz1  34781  reprpmtf1o  34785  reprdifc  34786  bnj1413  35193  cvmliftmolem1  35477  satf0suclem  35571  fwddifval  36358  neibastop1  36555  neibastop2lem  36556  fnejoin1  36564  filnetlem3  36576  filnetlem4  36577  weiunse  36664  numiunnum  36666  bj-imdirval2lem  37389  bj-imdirval3  37391  bj-imdirco  37397  dissneqlem  37547  aks6d1c2lem4  42449  sticksstones20  42488  aks6d1c6lem3  42494  psrbagres  42866  selvcllemh  42890  selvcllem4  42891  selvcllem5  42892  selvcl  42893  selvval2  42894  selvvvval  42895  evlselv  42897  selvadd  42898  selvmul  42899  fsuppssindlem2  42902  fsuppssind  42903  elrfi  43003  elrfirn2  43005  oaun3lem3  43685  nadd2rabex  43695  clcnvlem  43931  relexpss1d  44013  k0004lem2  44456  ixpssmapc  45385  restuni4  45432  restsubel  45464  wessf1ornlem  45496  disjinfi  45503  unirnmap  45519  inmap  45520  difmapsn  45523  unirnmapsn  45525  ssmapsn  45527  limsupre  45952  limsuppnfdlem  46012  limsuppnflem  46021  limsupmnflem  46031  limsupre2lem  46035  liminfval4  46100  liminfval3  46101  icccncfext  46198  dvdivcncf  46238  dvnprodlem1  46257  dvnprodlem2  46258  ovolsplit  46299  stoweidlem31  46342  stoweidlem53  46364  stoweidlem57  46368  stoweidlem59  46370  etransclem46  46591  salexct  46645  subsaluni  46671  fsumlesge0  46688  sge0iunmptlemfi  46724  sge0iunmptlemre  46726  meadjuni  46768  meadjiunlem  46776  omessle  46809  omecl  46814  isomenndlem  46841  caragencmpl  46846  ovnval2  46856  ovnval2b  46863  ovncvrrp  46875  ovncl  46878  hoidmvlelem2  46907  hoidmvlelem3  46908  ovncvr2  46922  ovnsubadd2lem  46956  ovnovollem3  46969  vonvolmbllem  46971  vonvolmbl  46972  sssmf  47049  incsmf  47053  issmflelem  47055  issmfle  47056  smfconst  47060  issmfgtlem  47066  issmfgt  47067  smfaddlem2  47075  decsmf  47078  issmfgelem  47080  issmfge  47081  nsssmfmbflem  47089  smfpimioo  47098  smfresal  47099  smfmullem4  47105  smfpimbor1lem1  47109  smf2id  47112  upwlksfval  48448  toplatglb  49313