Theorem ssexd 5265

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  abexd  5266  sselpwd  5269  moabex  5410  opabbrex  7420  soex  7872  fex2  7887  fabexd  7888  mapex  7892  funexw  7905  opabex2  8010  fnwelem  8081  fnse  8083  extmptsuppeq  8138  f1setex  8804  f1imaen2g  8962  fsuppss  9296  ordtypelem10  9442  oismo  9455  wofib  9460  wdom2d  9495  wdomd  9496  unxpwdom2  9503  ttrclexg  9644  djuexALT  9846  acni2  9968  fin1a2lem12  10333  hsmexlem1  10348  zorn2lem4  10421  ondomon  10485  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwe2lem11  10564  fpwwe2  10566  fpwwelem  10568  canthwelem  10573  pwfseqlem4  10585  hashf1lem1  14417  trclfv  14962  hashbcss  16975  strssd  17175  restid2  17393  divsfval  17511  mrieqv2d  17605  mrissmrcd  17606  mreexexlemd  17610  mreexexlem3d  17612  mreexexlem4d  17613  mreexdomd  17615  rescabs  17800  rescabs2  17801  resssetc  18059  resscatc  18076  estrres  18105  yonedalem1  18238  yonedalem21  18239  yonedalem3a  18240  yonedalem4c  18243  yonedalem22  18244  yonedalem3b  18245  yonedainv  18247  yonffthlem  18248  joinfval  18337  meetfval  18351  acsdomd  18523  ressmulgnnd  19054  gass  19276  pmtrfconj  19441  sylow2blem2  19596  dprdres  20005  dmdprdsplitlem  20014  primefld  20782  pwssplit0  21053  pwssplit1  21054  pwssplit2  21055  pwssplit3  21056  frlmsplit2  21753  frlmsslss  21754  opsrtoslem2  22034  evlsgsumadd  22074  evlsgsummul  22075  evls1gsumadd  22289  evls1gsummul  22290  evl1gsummul  22325  neiptoptop  23096  lpval  23104  neitr  23145  ordtbaslem  23153  ordtrest2  23169  cnrest2  23251  cnpresti  23253  cnprest  23254  cnprest2  23255  connsuba  23385  connsubclo  23389  unconn  23394  1stcelcls  23426  hausmapdom  23465  dissnref  23493  ptbasfi  23546  ptcls  23581  cnmpt2res  23642  qtopval2  23661  elqtop  23662  qtoprest  23682  ptuncnv  23772  ptunhmeo  23773  fsubbas  23832  elfm  23912  rnelfmlem  23917  rnelfm  23918  fmfnfmlem4  23922  flimclslem  23949  hauspwpwdom  23953  ptcmplem1  24017  cnextcn  24032  cnextfres1  24033  isust  24169  trust  24194  elutop  24198  restutop  24202  trcfilu  24258  cfiluweak  24259  psmetres2  24279  xmetres2  24326  fmcfil  25239  dvaddf  25909  dvmulf  25910  dvcmulf  25912  dvcof  25915  ulmss  26362  nosupno  27667  noinfno  27682  ssslts1  27765  ssslts2  27766  ltonsex  28254  perpln1  28778  perpln2  28779  isperp  28780  wksfval  29678  fnpreimac  32743  fisuppov1  32756  resf1o  32803  hashpss  32882  gsumpart  33124  gsumwrd2dccat  33139  cycpmco2lem5  33191  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspn  33307  erlval  33319  rlocval  33320  rlocbas  33328  fldgenval  33373  islinds5  33427  ellspds  33428  elrsp  33432  elrspunidl  33488  evlextv  33686  psrmonprod  33696  esplympl  33711  esplyind  33719  resssra  33731  lbslelsp  33742  lbsdiflsp0  33770  irngval  33829  ordtrest2NEW  34067  lmlim  34091  esummono  34198  esumrnmpt2  34212  esumpinfval  34217  elcarsg  34449  carsgmon  34458  carsggect  34462  reprval  34754  repr0  34755  reprsuc  34759  reprss  34761  reprinrn  34762  reprlt  34763  reprgt  34765  reprinfz1  34766  reprpmtf1o  34770  reprdifc  34771  bnj1413  35177  cvmliftmolem1  35463  satf0suclem  35557  fwddifval  36344  neibastop1  36541  neibastop2lem  36542  fnejoin1  36550  filnetlem3  36562  filnetlem4  36563  weiunse  36650  numiunnum  36652  bj-imdirval2lem  37496  bj-imdirval3  37498  bj-imdirco  37504  dissneqlem  37656  aks6d1c2lem4  42566  sticksstones20  42605  aks6d1c6lem3  42611  psrbagres  42989  selvcllemh  43013  selvcllem4  43014  selvcllem5  43015  selvcl  43016  selvval2  43017  selvvvval  43018  evlselv  43020  selvadd  43021  selvmul  43022  fsuppssindlem2  43025  fsuppssind  43026  elrfi  43126  elrfirn2  43128  oaun3lem3  43804  nadd2rabex  43814  clcnvlem  44050  relexpss1d  44132  k0004lem2  44575  ixpssmapc  45504  restuni4  45551  restsubel  45583  wessf1ornlem  45615  disjinfi  45622  unirnmap  45637  inmap  45638  difmapsn  45641  unirnmapsn  45643  ssmapsn  45645  limsupre  46069  limsuppnfdlem  46129  limsuppnflem  46138  limsupmnflem  46148  limsupre2lem  46152  liminfval4  46217  liminfval3  46218  icccncfext  46315  dvdivcncf  46355  dvnprodlem1  46374  dvnprodlem2  46375  ovolsplit  46416  stoweidlem31  46459  stoweidlem53  46481  stoweidlem57  46485  stoweidlem59  46487  etransclem46  46708  salexct  46762  subsaluni  46788  fsumlesge0  46805  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  meadjuni  46885  meadjiunlem  46893  omessle  46926  omecl  46931  isomenndlem  46958  caragencmpl  46963  ovnval2  46973  ovnval2b  46980  ovncvrrp  46992  ovncl  46995  hoidmvlelem2  47024  hoidmvlelem3  47025  ovncvr2  47039  ovnsubadd2lem  47073  ovnovollem3  47086  vonvolmbllem  47088  vonvolmbl  47089  sssmf  47166  incsmf  47170  issmflelem  47172  issmfle  47173  smfconst  47177  issmfgtlem  47183  issmfgt  47184  smfaddlem2  47192  decsmf  47195  issmfgelem  47197  issmfge  47198  nsssmfmbflem  47206  smfpimioo  47215  smfresal  47216  smfmullem4  47222  smfpimbor1lem1  47226  smf2id  47229  upwlksfval  48611  toplatglb  49476