Theorem ssexd 5220

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  sselpwd  5222  opabbrex  7201  soex  7620  fex2  7632  funexw  7647  opabex2  7749  fnwelem  7819  fnse  7821  extmptsuppeq  7848  f1imaen2g  8564  ordtypelem10  8985  oismo  8998  wofib  9003  wemapso  9009  wdom2d  9038  wdomd  9039  unxpwdom2  9046  djuexALT  9345  acni2  9466  fin1a2lem12  9827  hsmexlem1  9842  zorn2lem4  9915  fpwwe2lem2  10048  fpwwe2lem5  10050  fpwwe2lem12  10057  fpwwe2  10059  fpwwelem  10061  canthwelem  10066  pwfseqlem4  10078  trclfv  14354  hashbcss  16334  strssd  16527  restid2  16698  divsfval  16814  mrieqv2d  16904  mrissmrcd  16905  mreexexlemd  16909  mreexexlem3d  16911  mreexexlem4d  16912  mreexdomd  16914  rescabs  17097  rescabs2  17098  resssetc  17346  resscatc  17359  estrres  17383  yonedalem1  17516  yonedalem21  17517  yonedalem3a  17518  yonedalem4c  17521  yonedalem22  17522  yonedalem3b  17523  yonedainv  17525  yonffthlem  17526  joinfval  17605  meetfval  17619  acsdomd  17785  gass  18425  permsetex  18492  pmtrfconj  18588  sylow2blem2  18740  dprdres  19144  dmdprdsplitlem  19153  primefld  19578  pwssplit0  19824  pwssplit1  19825  pwssplit2  19826  pwssplit3  19827  opsrtoslem2  20259  evlsgsumadd  20298  evlsgsummul  20299  evls1gsumadd  20481  evls1gsummul  20482  evl1gsummul  20517  frlmsplit2  20911  frlmsslss  20912  neiptoptop  21733  lpval  21741  neitr  21782  ordtbaslem  21790  ordtrest2  21806  cnrest2  21888  cnpresti  21890  cnprest  21891  cnprest2  21892  connsuba  22022  connsubclo  22026  unconn  22031  1stcelcls  22063  hausmapdom  22102  dissnref  22130  ptbasfi  22183  ptcls  22218  cnmpt2res  22279  qtopval2  22298  elqtop  22299  qtoprest  22319  ptuncnv  22409  ptunhmeo  22410  fsubbas  22469  elfm  22549  rnelfmlem  22554  rnelfm  22555  fmfnfmlem4  22559  flimclslem  22586  hauspwpwdom  22590  ptcmplem1  22654  cnextcn  22669  cnextfres1  22670  isust  22806  trust  22832  elutop  22836  restutop  22840  trcfilu  22897  cfiluweak  22898  psmetres2  22918  xmetres2  22965  fmcfil  23869  dvaddf  24533  dvmulf  24534  dvcmulf  24536  dvcof  24539  ulmss  24979  perpln1  26490  perpln2  26491  isperp  26492  wksfval  27385  fnpreimac  30410  resf1o  30460  cycpmco2lem5  30767  islinds5  30927  ellspds  30928  lbsdiflsp0  31017  ordtrest2NEW  31161  lmlim  31185  esummono  31308  esumrnmpt2  31322  esumpinfval  31327  elcarsg  31558  carsgmon  31567  carsggect  31571  reprval  31876  repr0  31877  reprsuc  31881  reprss  31883  reprinrn  31884  reprlt  31885  reprgt  31887  reprinfz1  31888  reprpmtf1o  31892  reprdifc  31893  bnj1413  32302  cvmliftmolem1  32523  satf0suclem  32617  nosupno  33198  sssslt1  33255  sssslt2  33256  fwddifval  33618  neibastop1  33702  neibastop2lem  33703  fnejoin1  33711  filnetlem3  33723  filnetlem4  33724  bj-imdirval2  34467  bj-imdirval3  34468  dissneqlem  34615  selvval2lemn  39128  selvval2lem4  39129  selvval2lem5  39130  selvcl  39131  elrfi  39284  elrfirn2  39286  clcnvlem  39976  relexpss1d  40043  k0004lem2  40491  ixpssmapc  41329  restuni4  41380  wessf1ornlem  41438  unirnmap  41464  inmap  41465  difmapsn  41468  unirnmapsn  41470  ssmapsn  41472  limsupre  41915  limsuppnfdlem  41975  limsuppnflem  41984  limsupmnflem  41994  limsupre2lem  41998  liminfval4  42063  liminfval3  42064  icccncfext  42163  dvdivcncf  42205  dvnprodlem1  42224  dvnprodlem2  42225  ovolsplit  42267  stoweidlem31  42310  stoweidlem53  42332  stoweidlem57  42336  stoweidlem59  42338  etransclem46  42559  saliuncl  42601  salexct  42611  subsaluni  42637  fsumlesge0  42653  sge0f1o  42658  sge0iunmptlemfi  42689  sge0iunmptlemre  42691  meadjuni  42733  meadjiunlem  42741  omessle  42774  omecl  42779  isomenndlem  42806  caragencmpl  42811  ovnval2  42821  ovnval2b  42828  ovncvrrp  42840  ovncl  42843  hoidmvlelem2  42872  hoidmvlelem3  42873  ovncvr2  42887  ovnsubadd2lem  42921  ovnovollem3  42934  vonvolmbllem  42936  vonvolmbl  42937  sssmf  43009  incsmf  43013  issmflelem  43015  issmfle  43016  smfconst  43020  issmfgtlem  43026  issmfgt  43027  smfaddlem2  43034  decsmf  43037  issmfgelem  43039  issmfge  43040  nsssmfmbflem  43048  smfpimioo  43056  smfresal  43057  smfmullem4  43063  smfpimbor1lem1  43067  smf2id  43070  upwlksfval  44004