Theorem ssexd 5243

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sselpwd  5245  opabbrex  7306  soex  7742  fex2  7754  funexw  7768  opabex2  7870  fnwelem  7943  fnse  7945  extmptsuppeq  7975  f1setex  8603  f1imaen2g  8756  ordtypelem10  9216  oismo  9229  wofib  9234  wdom2d  9269  wdomd  9270  unxpwdom2  9277  djuexALT  9611  acni2  9733  fin1a2lem12  10098  hsmexlem1  10113  zorn2lem4  10186  fpwwe2lem2  10319  fpwwe2lem4  10321  fpwwe2lem11  10328  fpwwe2  10330  fpwwelem  10332  canthwelem  10337  pwfseqlem4  10349  hashf1lem1  14096  trclfv  14639  hashbcss  16633  strssd  16835  restid2  17058  divsfval  17175  mrieqv2d  17265  mrissmrcd  17266  mreexexlemd  17270  mreexexlem3d  17272  mreexexlem4d  17273  mreexdomd  17275  rescabs  17464  rescabs2  17465  resssetc  17723  resscatc  17740  estrres  17772  yonedalem1  17906  yonedalem21  17907  yonedalem3a  17908  yonedalem4c  17911  yonedalem22  17912  yonedalem3b  17913  yonedainv  17915  yonffthlem  17916  joinfval  18006  meetfval  18020  acsdomd  18190  gass  18822  permsetexOLD  18892  pmtrfconj  18989  sylow2blem2  19141  dprdres  19546  dmdprdsplitlem  19555  primefld  19988  pwssplit0  20235  pwssplit1  20236  pwssplit2  20237  pwssplit3  20238  frlmsplit2  20890  frlmsslss  20891  opsrtoslem2  21173  evlsgsumadd  21211  evlsgsummul  21212  evls1gsumadd  21400  evls1gsummul  21401  evl1gsummul  21436  neiptoptop  22190  lpval  22198  neitr  22239  ordtbaslem  22247  ordtrest2  22263  cnrest2  22345  cnpresti  22347  cnprest  22348  cnprest2  22349  connsuba  22479  connsubclo  22483  unconn  22488  1stcelcls  22520  hausmapdom  22559  dissnref  22587  ptbasfi  22640  ptcls  22675  cnmpt2res  22736  qtopval2  22755  elqtop  22756  qtoprest  22776  ptuncnv  22866  ptunhmeo  22867  fsubbas  22926  elfm  23006  rnelfmlem  23011  rnelfm  23012  fmfnfmlem4  23016  flimclslem  23043  hauspwpwdom  23047  ptcmplem1  23111  cnextcn  23126  cnextfres1  23127  isust  23263  trust  23289  elutop  23293  restutop  23297  trcfilu  23354  cfiluweak  23355  psmetres2  23375  xmetres2  23422  fmcfil  24341  dvaddf  25011  dvmulf  25012  dvcmulf  25014  dvcof  25017  ulmss  25461  perpln1  26975  perpln2  26976  isperp  26977  wksfval  27879  fnpreimac  30910  resf1o  30967  gsumpart  31217  cycpmco2lem5  31299  islinds5  31465  ellspds  31466  elrsp  31471  elrspunidl  31508  lbsdiflsp0  31609  ordtrest2NEW  31775  lmlim  31799  esummono  31922  esumrnmpt2  31936  esumpinfval  31941  elcarsg  32172  carsgmon  32181  carsggect  32185  reprval  32490  repr0  32491  reprsuc  32495  reprss  32497  reprinrn  32498  reprlt  32499  reprgt  32501  reprinfz1  32502  reprpmtf1o  32506  reprdifc  32507  bnj1413  32915  cvmliftmolem1  33143  satf0suclem  33237  ttrclexg  33709  nosupno  33833  noinfno  33848  sssslt1  33916  sssslt2  33917  fwddifval  34391  neibastop1  34475  neibastop2lem  34476  fnejoin1  34484  filnetlem3  34496  filnetlem4  34497  bj-imdirval2lem  35280  bj-imdirval3  35282  bj-imdirco  35288  dissneqlem  35438  sticksstones20  40050  selvval2lemn  40153  selvval2lem4  40154  selvval2lem5  40155  selvcl  40156  fsuppssindlem2  40204  fsuppssind  40205  elrfi  40432  elrfirn2  40434  clcnvlem  41120  relexpss1d  41202  k0004lem2  41647  ixpssmapc  42511  restuni4  42559  wessf1ornlem  42611  disjinfi  42620  unirnmap  42637  inmap  42638  difmapsn  42641  unirnmapsn  42643  ssmapsn  42645  limsupre  43072  limsuppnfdlem  43132  limsuppnflem  43141  limsupmnflem  43151  limsupre2lem  43155  liminfval4  43220  liminfval3  43221  icccncfext  43318  dvdivcncf  43358  dvnprodlem1  43377  dvnprodlem2  43378  ovolsplit  43419  stoweidlem31  43462  stoweidlem53  43484  stoweidlem57  43488  stoweidlem59  43490  etransclem46  43711  saliuncl  43753  salexct  43763  subsaluni  43789  fsumlesge0  43805  sge0f1o  43810  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  meadjuni  43885  meadjiunlem  43893  omessle  43926  omecl  43931  isomenndlem  43958  caragencmpl  43963  ovnval2  43973  ovnval2b  43980  ovncvrrp  43992  ovncl  43995  hoidmvlelem2  44024  hoidmvlelem3  44025  ovncvr2  44039  ovnsubadd2lem  44073  ovnovollem3  44086  vonvolmbllem  44088  vonvolmbl  44089  sssmf  44161  incsmf  44165  issmflelem  44167  issmfle  44168  smfconst  44172  issmfgtlem  44178  issmfgt  44179  smfaddlem2  44186  decsmf  44189  issmfgelem  44191  issmfge  44192  nsssmfmbflem  44200  smfpimioo  44208  smfresal  44209  smfmullem4  44215  smfpimbor1lem1  44219  smf2id  44222  upwlksfval  45185  toplatglb  46175