Theorem ssexd 5329

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  abexd  5330  sselpwd  5333  opabbrex  7483  soex  7943  fex2  7956  fabexd  7957  mapex  7961  funexw  7974  opabex2  8080  fnwelem  8154  fnse  8156  extmptsuppeq  8211  f1setex  8895  f1imaen2g  9053  fsuppss  9420  ordtypelem10  9564  oismo  9577  wofib  9582  wdom2d  9617  wdomd  9618  unxpwdom2  9625  ttrclexg  9760  djuexALT  9959  acni2  10083  fin1a2lem12  10448  hsmexlem1  10463  zorn2lem4  10536  fpwwe2lem2  10669  fpwwe2lem4  10671  fpwwe2lem11  10678  fpwwe2  10680  fpwwelem  10682  canthwelem  10687  pwfseqlem4  10699  hashf1lem1  14490  trclfv  15035  hashbcss  17037  strssd  17239  restid2  17476  divsfval  17593  mrieqv2d  17683  mrissmrcd  17684  mreexexlemd  17688  mreexexlem3d  17690  mreexexlem4d  17691  mreexdomd  17693  rescabs  17882  rescabsOLD  17883  rescabs2  17884  resssetc  18145  resscatc  18162  estrres  18194  yonedalem1  18328  yonedalem21  18329  yonedalem3a  18330  yonedalem4c  18333  yonedalem22  18334  yonedalem3b  18335  yonedainv  18337  yonffthlem  18338  joinfval  18430  meetfval  18444  acsdomd  18614  ressmulgnnd  19108  gass  19331  pmtrfconj  19498  sylow2blem2  19653  dprdres  20062  dmdprdsplitlem  20071  primefld  20822  pwssplit0  21074  pwssplit1  21075  pwssplit2  21076  pwssplit3  21077  frlmsplit2  21810  frlmsslss  21811  opsrtoslem2  22097  evlsgsumadd  22132  evlsgsummul  22133  evls1gsumadd  22343  evls1gsummul  22344  evl1gsummul  22379  neiptoptop  23154  lpval  23162  neitr  23203  ordtbaslem  23211  ordtrest2  23227  cnrest2  23309  cnpresti  23311  cnprest  23312  cnprest2  23313  connsuba  23443  connsubclo  23447  unconn  23452  1stcelcls  23484  hausmapdom  23523  dissnref  23551  ptbasfi  23604  ptcls  23639  cnmpt2res  23700  qtopval2  23719  elqtop  23720  qtoprest  23740  ptuncnv  23830  ptunhmeo  23831  fsubbas  23890  elfm  23970  rnelfmlem  23975  rnelfm  23976  fmfnfmlem4  23980  flimclslem  24007  hauspwpwdom  24011  ptcmplem1  24075  cnextcn  24090  cnextfres1  24091  isust  24227  trust  24253  elutop  24257  restutop  24261  trcfilu  24318  cfiluweak  24319  psmetres2  24339  xmetres2  24386  fmcfil  25319  dvaddf  25993  dvmulf  25994  dvcmulf  25996  dvcof  26000  ulmss  26454  nosupno  27762  noinfno  27777  sssslt1  27854  sssslt2  27855  sltonex  28298  perpln1  28732  perpln2  28733  isperp  28734  wksfval  29641  fnpreimac  32687  fisuppov1  32697  resf1o  32747  gsumpart  33042  gsumwrd2dccat  33052  cycpmco2lem5  33132  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  erlval  33244  rlocval  33245  rlocbas  33253  fldgenval  33293  islinds5  33374  ellspds  33375  elrsp  33379  elrspunidl  33435  resssra  33616  lbsdiflsp0  33653  irngval  33699  ordtrest2NEW  33883  lmlim  33907  esummono  34034  esumrnmpt2  34048  esumpinfval  34053  elcarsg  34286  carsgmon  34295  carsggect  34299  reprval  34603  repr0  34604  reprsuc  34608  reprss  34610  reprinrn  34611  reprlt  34612  reprgt  34614  reprinfz1  34615  reprpmtf1o  34619  reprdifc  34620  bnj1413  35027  cvmliftmolem1  35265  satf0suclem  35359  fwddifval  36143  neibastop1  36341  neibastop2lem  36342  fnejoin1  36350  filnetlem3  36362  filnetlem4  36363  weiunse  36450  numiunnum  36452  bj-imdirval2lem  37164  bj-imdirval3  37166  bj-imdirco  37172  dissneqlem  37322  aks6d1c2lem4  42108  sticksstones20  42147  aks6d1c6lem3  42153  psrbagres  42532  selvcllemh  42566  selvcllem4  42567  selvcllem5  42568  selvcl  42569  selvval2  42570  selvvvval  42571  evlselv  42573  selvadd  42574  selvmul  42575  fsuppssindlem2  42578  fsuppssind  42579  elrfi  42681  elrfirn2  42683  oaun3lem3  43365  nadd2rabex  43375  clcnvlem  43612  relexpss1d  43694  k0004lem2  44137  ixpssmapc  45012  restuni4  45060  restsubel  45095  wessf1ornlem  45127  disjinfi  45134  unirnmap  45150  inmap  45151  difmapsn  45154  unirnmapsn  45156  ssmapsn  45158  limsupre  45596  limsuppnfdlem  45656  limsuppnflem  45665  limsupmnflem  45675  limsupre2lem  45679  liminfval4  45744  liminfval3  45745  icccncfext  45842  dvdivcncf  45882  dvnprodlem1  45901  dvnprodlem2  45902  ovolsplit  45943  stoweidlem31  45986  stoweidlem53  46008  stoweidlem57  46012  stoweidlem59  46014  etransclem46  46235  salexct  46289  subsaluni  46315  fsumlesge0  46332  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  meadjuni  46412  meadjiunlem  46420  omessle  46453  omecl  46458  isomenndlem  46485  caragencmpl  46490  ovnval2  46500  ovnval2b  46507  ovncvrrp  46519  ovncl  46522  hoidmvlelem2  46551  hoidmvlelem3  46552  ovncvr2  46566  ovnsubadd2lem  46600  ovnovollem3  46613  vonvolmbllem  46615  vonvolmbl  46616  sssmf  46693  incsmf  46697  issmflelem  46699  issmfle  46700  smfconst  46704  issmfgtlem  46710  issmfgt  46711  smfaddlem2  46719  decsmf  46722  issmfgelem  46724  issmfge  46725  nsssmfmbflem  46733  smfpimioo  46742  smfresal  46743  smfmullem4  46749  smfpimbor1lem1  46753  smf2id  46756  upwlksfval  47978  toplatglb  48789