Theorem ssexd 5274

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  abexd  5275  sselpwd  5278  opabbrex  7422  soex  7877  fex2  7892  fabexd  7893  mapex  7897  funexw  7910  opabex2  8015  fnwelem  8087  fnse  8089  extmptsuppeq  8144  f1setex  8807  f1imaen2g  8963  fsuppss  9310  ordtypelem10  9456  oismo  9469  wofib  9474  wdom2d  9509  wdomd  9510  unxpwdom2  9517  ttrclexg  9652  djuexALT  9851  acni2  9975  fin1a2lem12  10340  hsmexlem1  10355  zorn2lem4  10428  fpwwe2lem2  10561  fpwwe2lem4  10563  fpwwe2lem11  10570  fpwwe2  10572  fpwwelem  10574  canthwelem  10579  pwfseqlem4  10591  hashf1lem1  14396  trclfv  14942  hashbcss  16951  strssd  17151  restid2  17369  divsfval  17486  mrieqv2d  17580  mrissmrcd  17581  mreexexlemd  17585  mreexexlem3d  17587  mreexexlem4d  17588  mreexdomd  17590  rescabs  17775  rescabs2  17776  resssetc  18034  resscatc  18051  estrres  18080  yonedalem1  18213  yonedalem21  18214  yonedalem3a  18215  yonedalem4c  18218  yonedalem22  18219  yonedalem3b  18220  yonedainv  18222  yonffthlem  18223  joinfval  18312  meetfval  18326  acsdomd  18498  ressmulgnnd  18992  gass  19215  pmtrfconj  19380  sylow2blem2  19535  dprdres  19944  dmdprdsplitlem  19953  primefld  20725  pwssplit0  20997  pwssplit1  20998  pwssplit2  20999  pwssplit3  21000  frlmsplit2  21715  frlmsslss  21716  opsrtoslem2  21996  evlsgsumadd  22031  evlsgsummul  22032  evls1gsumadd  22244  evls1gsummul  22245  evl1gsummul  22280  neiptoptop  23051  lpval  23059  neitr  23100  ordtbaslem  23108  ordtrest2  23124  cnrest2  23206  cnpresti  23208  cnprest  23209  cnprest2  23210  connsuba  23340  connsubclo  23344  unconn  23349  1stcelcls  23381  hausmapdom  23420  dissnref  23448  ptbasfi  23501  ptcls  23536  cnmpt2res  23597  qtopval2  23616  elqtop  23617  qtoprest  23637  ptuncnv  23727  ptunhmeo  23728  fsubbas  23787  elfm  23867  rnelfmlem  23872  rnelfm  23873  fmfnfmlem4  23877  flimclslem  23904  hauspwpwdom  23908  ptcmplem1  23972  cnextcn  23987  cnextfres1  23988  isust  24124  trust  24150  elutop  24154  restutop  24158  trcfilu  24214  cfiluweak  24215  psmetres2  24235  xmetres2  24282  fmcfil  25205  dvaddf  25878  dvmulf  25879  dvcmulf  25881  dvcof  25885  ulmss  26339  nosupno  27648  noinfno  27663  sssslt1  27741  sssslt2  27742  sltonex  28203  perpln1  28690  perpln2  28691  isperp  28692  wksfval  29590  fnpreimac  32645  fisuppov1  32656  resf1o  32703  hashpss  32784  gsumpart  33040  gsumwrd2dccat  33050  cycpmco2lem5  33102  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspn  33213  erlval  33225  rlocval  33226  rlocbas  33234  fldgenval  33278  islinds5  33331  ellspds  33332  elrsp  33336  elrspunidl  33392  resssra  33576  lbslelsp  33586  lbsdiflsp0  33615  irngval  33673  ordtrest2NEW  33906  lmlim  33930  esummono  34037  esumrnmpt2  34051  esumpinfval  34056  elcarsg  34289  carsgmon  34298  carsggect  34302  reprval  34594  repr0  34595  reprsuc  34599  reprss  34601  reprinrn  34602  reprlt  34603  reprgt  34605  reprinfz1  34606  reprpmtf1o  34610  reprdifc  34611  bnj1413  35018  cvmliftmolem1  35261  satf0suclem  35355  fwddifval  36143  neibastop1  36340  neibastop2lem  36341  fnejoin1  36349  filnetlem3  36361  filnetlem4  36362  weiunse  36449  numiunnum  36451  bj-imdirval2lem  37163  bj-imdirval3  37165  bj-imdirco  37171  dissneqlem  37321  aks6d1c2lem4  42108  sticksstones20  42147  aks6d1c6lem3  42153  psrbagres  42527  selvcllemh  42561  selvcllem4  42562  selvcllem5  42563  selvcl  42564  selvval2  42565  selvvvval  42566  evlselv  42568  selvadd  42569  selvmul  42570  fsuppssindlem2  42573  fsuppssind  42574  elrfi  42675  elrfirn2  42677  oaun3lem3  43358  nadd2rabex  43368  clcnvlem  43605  relexpss1d  43687  k0004lem2  44130  ixpssmapc  45060  restuni4  45108  restsubel  45140  wessf1ornlem  45172  disjinfi  45179  unirnmap  45195  inmap  45196  difmapsn  45199  unirnmapsn  45201  ssmapsn  45203  limsupre  45632  limsuppnfdlem  45692  limsuppnflem  45701  limsupmnflem  45711  limsupre2lem  45715  liminfval4  45780  liminfval3  45781  icccncfext  45878  dvdivcncf  45918  dvnprodlem1  45937  dvnprodlem2  45938  ovolsplit  45979  stoweidlem31  46022  stoweidlem53  46044  stoweidlem57  46048  stoweidlem59  46050  etransclem46  46271  salexct  46325  subsaluni  46351  fsumlesge0  46368  sge0iunmptlemfi  46404  sge0iunmptlemre  46406  meadjuni  46448  meadjiunlem  46456  omessle  46489  omecl  46494  isomenndlem  46521  caragencmpl  46526  ovnval2  46536  ovnval2b  46543  ovncvrrp  46555  ovncl  46558  hoidmvlelem2  46587  hoidmvlelem3  46588  ovncvr2  46602  ovnsubadd2lem  46636  ovnovollem3  46649  vonvolmbllem  46651  vonvolmbl  46652  sssmf  46729  incsmf  46733  issmflelem  46735  issmfle  46736  smfconst  46740  issmfgtlem  46746  issmfgt  46747  smfaddlem2  46755  decsmf  46758  issmfgelem  46760  issmfge  46761  nsssmfmbflem  46769  smfpimioo  46778  smfresal  46779  smfmullem4  46785  smfpimbor1lem1  46789  smf2id  46792  upwlksfval  48116  toplatglb  48982