Theorem ssexd 5282

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917

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 2702  ax-sep 5254

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  abexd  5283  sselpwd  5286  opabbrex  7443  soex  7900  fex2  7915  fabexd  7916  mapex  7920  funexw  7933  opabex2  8039  fnwelem  8113  fnse  8115  extmptsuppeq  8170  f1setex  8833  f1imaen2g  8989  fsuppss  9341  ordtypelem10  9487  oismo  9500  wofib  9505  wdom2d  9540  wdomd  9541  unxpwdom2  9548  ttrclexg  9683  djuexALT  9882  acni2  10006  fin1a2lem12  10371  hsmexlem1  10386  zorn2lem4  10459  fpwwe2lem2  10592  fpwwe2lem4  10594  fpwwe2lem11  10601  fpwwe2  10603  fpwwelem  10605  canthwelem  10610  pwfseqlem4  10622  hashf1lem1  14427  trclfv  14973  hashbcss  16982  strssd  17182  restid2  17400  divsfval  17517  mrieqv2d  17607  mrissmrcd  17608  mreexexlemd  17612  mreexexlem3d  17614  mreexexlem4d  17615  mreexdomd  17617  rescabs  17802  rescabs2  17803  resssetc  18061  resscatc  18078  estrres  18107  yonedalem1  18240  yonedalem21  18241  yonedalem3a  18242  yonedalem4c  18245  yonedalem22  18246  yonedalem3b  18247  yonedainv  18249  yonffthlem  18250  joinfval  18339  meetfval  18353  acsdomd  18523  ressmulgnnd  19017  gass  19240  pmtrfconj  19403  sylow2blem2  19558  dprdres  19967  dmdprdsplitlem  19976  primefld  20721  pwssplit0  20972  pwssplit1  20973  pwssplit2  20974  pwssplit3  20975  frlmsplit2  21689  frlmsslss  21690  opsrtoslem2  21970  evlsgsumadd  22005  evlsgsummul  22006  evls1gsumadd  22218  evls1gsummul  22219  evl1gsummul  22254  neiptoptop  23025  lpval  23033  neitr  23074  ordtbaslem  23082  ordtrest2  23098  cnrest2  23180  cnpresti  23182  cnprest  23183  cnprest2  23184  connsuba  23314  connsubclo  23318  unconn  23323  1stcelcls  23355  hausmapdom  23394  dissnref  23422  ptbasfi  23475  ptcls  23510  cnmpt2res  23571  qtopval2  23590  elqtop  23591  qtoprest  23611  ptuncnv  23701  ptunhmeo  23702  fsubbas  23761  elfm  23841  rnelfmlem  23846  rnelfm  23847  fmfnfmlem4  23851  flimclslem  23878  hauspwpwdom  23882  ptcmplem1  23946  cnextcn  23961  cnextfres1  23962  isust  24098  trust  24124  elutop  24128  restutop  24132  trcfilu  24188  cfiluweak  24189  psmetres2  24209  xmetres2  24256  fmcfil  25179  dvaddf  25852  dvmulf  25853  dvcmulf  25855  dvcof  25859  ulmss  26313  nosupno  27622  noinfno  27637  sssslt1  27714  sssslt2  27715  sltonex  28170  perpln1  28644  perpln2  28645  isperp  28646  wksfval  29544  fnpreimac  32602  fisuppov1  32613  resf1o  32660  hashpss  32741  gsumpart  33004  gsumwrd2dccat  33014  cycpmco2lem5  33094  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspn  33204  erlval  33216  rlocval  33217  rlocbas  33225  fldgenval  33269  islinds5  33345  ellspds  33346  elrsp  33350  elrspunidl  33406  resssra  33590  lbslelsp  33600  lbsdiflsp0  33629  irngval  33687  ordtrest2NEW  33920  lmlim  33944  esummono  34051  esumrnmpt2  34065  esumpinfval  34070  elcarsg  34303  carsgmon  34312  carsggect  34316  reprval  34608  repr0  34609  reprsuc  34613  reprss  34615  reprinrn  34616  reprlt  34617  reprgt  34619  reprinfz1  34620  reprpmtf1o  34624  reprdifc  34625  bnj1413  35032  cvmliftmolem1  35275  satf0suclem  35369  fwddifval  36157  neibastop1  36354  neibastop2lem  36355  fnejoin1  36363  filnetlem3  36375  filnetlem4  36376  weiunse  36463  numiunnum  36465  bj-imdirval2lem  37177  bj-imdirval3  37179  bj-imdirco  37185  dissneqlem  37335  aks6d1c2lem4  42122  sticksstones20  42161  aks6d1c6lem3  42167  psrbagres  42541  selvcllemh  42575  selvcllem4  42576  selvcllem5  42577  selvcl  42578  selvval2  42579  selvvvval  42580  evlselv  42582  selvadd  42583  selvmul  42584  fsuppssindlem2  42587  fsuppssind  42588  elrfi  42689  elrfirn2  42691  oaun3lem3  43372  nadd2rabex  43382  clcnvlem  43619  relexpss1d  43701  k0004lem2  44144  ixpssmapc  45074  restuni4  45122  restsubel  45154  wessf1ornlem  45186  disjinfi  45193  unirnmap  45209  inmap  45210  difmapsn  45213  unirnmapsn  45215  ssmapsn  45217  limsupre  45646  limsuppnfdlem  45706  limsuppnflem  45715  limsupmnflem  45725  limsupre2lem  45729  liminfval4  45794  liminfval3  45795  icccncfext  45892  dvdivcncf  45932  dvnprodlem1  45951  dvnprodlem2  45952  ovolsplit  45993  stoweidlem31  46036  stoweidlem53  46058  stoweidlem57  46062  stoweidlem59  46064  etransclem46  46285  salexct  46339  subsaluni  46365  fsumlesge0  46382  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  meadjuni  46462  meadjiunlem  46470  omessle  46503  omecl  46508  isomenndlem  46535  caragencmpl  46540  ovnval2  46550  ovnval2b  46557  ovncvrrp  46569  ovncl  46572  hoidmvlelem2  46601  hoidmvlelem3  46602  ovncvr2  46616  ovnsubadd2lem  46650  ovnovollem3  46663  vonvolmbllem  46665  vonvolmbl  46666  sssmf  46743  incsmf  46747  issmflelem  46749  issmfle  46750  smfconst  46754  issmfgtlem  46760  issmfgt  46761  smfaddlem2  46769  decsmf  46772  issmfgelem  46774  issmfge  46775  nsssmfmbflem  46783  smfpimioo  46792  smfresal  46793  smfmullem4  46799  smfpimbor1lem1  46803  smf2id  46806  upwlksfval  48127  toplatglb  48993