Theorem ssexd 5260

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  abexd  5261  sselpwd  5264  opabbrex  7399  soex  7851  fex2  7866  fabexd  7867  mapex  7871  funexw  7884  opabex2  7989  fnwelem  8061  fnse  8063  extmptsuppeq  8118  f1setex  8781  f1imaen2g  8937  fsuppss  9267  ordtypelem10  9413  oismo  9426  wofib  9431  wdom2d  9466  wdomd  9467  unxpwdom2  9474  ttrclexg  9613  djuexALT  9815  acni2  9937  fin1a2lem12  10302  hsmexlem1  10317  zorn2lem4  10390  fpwwe2lem2  10523  fpwwe2lem4  10525  fpwwe2lem11  10532  fpwwe2  10534  fpwwelem  10536  canthwelem  10541  pwfseqlem4  10553  hashf1lem1  14362  trclfv  14907  hashbcss  16916  strssd  17116  restid2  17334  divsfval  17451  mrieqv2d  17545  mrissmrcd  17546  mreexexlemd  17550  mreexexlem3d  17552  mreexexlem4d  17553  mreexdomd  17555  rescabs  17740  rescabs2  17741  resssetc  17999  resscatc  18016  estrres  18045  yonedalem1  18178  yonedalem21  18179  yonedalem3a  18180  yonedalem4c  18183  yonedalem22  18184  yonedalem3b  18185  yonedainv  18187  yonffthlem  18188  joinfval  18277  meetfval  18291  acsdomd  18463  ressmulgnnd  18991  gass  19213  pmtrfconj  19378  sylow2blem2  19533  dprdres  19942  dmdprdsplitlem  19951  primefld  20720  pwssplit0  20992  pwssplit1  20993  pwssplit2  20994  pwssplit3  20995  frlmsplit2  21710  frlmsslss  21711  opsrtoslem2  21991  evlsgsumadd  22026  evlsgsummul  22027  evls1gsumadd  22239  evls1gsummul  22240  evl1gsummul  22275  neiptoptop  23046  lpval  23054  neitr  23095  ordtbaslem  23103  ordtrest2  23119  cnrest2  23201  cnpresti  23203  cnprest  23204  cnprest2  23205  connsuba  23335  connsubclo  23339  unconn  23344  1stcelcls  23376  hausmapdom  23415  dissnref  23443  ptbasfi  23496  ptcls  23531  cnmpt2res  23592  qtopval2  23611  elqtop  23612  qtoprest  23632  ptuncnv  23722  ptunhmeo  23723  fsubbas  23782  elfm  23862  rnelfmlem  23867  rnelfm  23868  fmfnfmlem4  23872  flimclslem  23899  hauspwpwdom  23903  ptcmplem1  23967  cnextcn  23982  cnextfres1  23983  isust  24119  trust  24144  elutop  24148  restutop  24152  trcfilu  24208  cfiluweak  24209  psmetres2  24229  xmetres2  24276  fmcfil  25199  dvaddf  25872  dvmulf  25873  dvcmulf  25875  dvcof  25879  ulmss  26333  nosupno  27642  noinfno  27657  sssslt1  27736  sssslt2  27737  sltonex  28199  perpln1  28688  perpln2  28689  isperp  28690  wksfval  29588  fnpreimac  32653  fisuppov1  32664  resf1o  32713  hashpss  32791  gsumpart  33037  gsumwrd2dccat  33047  cycpmco2lem5  33099  elrgspnlem1  33209  elrgspnlem2  33210  elrgspnlem3  33211  elrgspnlem4  33212  elrgspn  33213  erlval  33225  rlocval  33226  rlocbas  33234  fldgenval  33278  islinds5  33332  ellspds  33333  elrsp  33337  elrspunidl  33393  esplympl  33588  resssra  33599  lbslelsp  33610  lbsdiflsp0  33639  irngval  33698  ordtrest2NEW  33936  lmlim  33960  esummono  34067  esumrnmpt2  34081  esumpinfval  34086  elcarsg  34318  carsgmon  34327  carsggect  34331  reprval  34623  repr0  34624  reprsuc  34628  reprss  34630  reprinrn  34631  reprlt  34632  reprgt  34634  reprinfz1  34635  reprpmtf1o  34639  reprdifc  34640  bnj1413  35047  cvmliftmolem1  35325  satf0suclem  35419  fwddifval  36206  neibastop1  36403  neibastop2lem  36404  fnejoin1  36412  filnetlem3  36424  filnetlem4  36425  weiunse  36512  numiunnum  36514  bj-imdirval2lem  37226  bj-imdirval3  37228  bj-imdirco  37234  dissneqlem  37384  aks6d1c2lem4  42219  sticksstones20  42258  aks6d1c6lem3  42264  psrbagres  42638  selvcllemh  42672  selvcllem4  42673  selvcllem5  42674  selvcl  42675  selvval2  42676  selvvvval  42677  evlselv  42679  selvadd  42680  selvmul  42681  fsuppssindlem2  42684  fsuppssind  42685  elrfi  42786  elrfirn2  42788  oaun3lem3  43468  nadd2rabex  43478  clcnvlem  43715  relexpss1d  43797  k0004lem2  44240  ixpssmapc  45169  restuni4  45217  restsubel  45249  wessf1ornlem  45281  disjinfi  45288  unirnmap  45304  inmap  45305  difmapsn  45308  unirnmapsn  45310  ssmapsn  45312  limsupre  45738  limsuppnfdlem  45798  limsuppnflem  45807  limsupmnflem  45817  limsupre2lem  45821  liminfval4  45886  liminfval3  45887  icccncfext  45984  dvdivcncf  46024  dvnprodlem1  46043  dvnprodlem2  46044  ovolsplit  46085  stoweidlem31  46128  stoweidlem53  46150  stoweidlem57  46154  stoweidlem59  46156  etransclem46  46377  salexct  46431  subsaluni  46457  fsumlesge0  46474  sge0iunmptlemfi  46510  sge0iunmptlemre  46512  meadjuni  46554  meadjiunlem  46562  omessle  46595  omecl  46600  isomenndlem  46627  caragencmpl  46632  ovnval2  46642  ovnval2b  46649  ovncvrrp  46661  ovncl  46664  hoidmvlelem2  46693  hoidmvlelem3  46694  ovncvr2  46708  ovnsubadd2lem  46742  ovnovollem3  46755  vonvolmbllem  46757  vonvolmbl  46758  sssmf  46835  incsmf  46839  issmflelem  46841  issmfle  46842  smfconst  46846  issmfgtlem  46852  issmfgt  46853  smfaddlem2  46861  decsmf  46864  issmfgelem  46866  issmfge  46867  nsssmfmbflem  46875  smfpimioo  46884  smfresal  46885  smfmullem4  46891  smfpimbor1lem1  46895  smf2id  46898  upwlksfval  48234  toplatglb  49100