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  9654  djuexALT  9853  acni2  9977  fin1a2lem12  10342  hsmexlem1  10357  zorn2lem4  10430  fpwwe2lem2  10563  fpwwe2lem4  10565  fpwwe2lem11  10572  fpwwe2  10574  fpwwelem  10576  canthwelem  10581  pwfseqlem4  10593  hashf1lem1  14398  trclfv  14943  hashbcss  16952  strssd  17152  restid2  17370  divsfval  17487  mrieqv2d  17581  mrissmrcd  17582  mreexexlemd  17586  mreexexlem3d  17588  mreexexlem4d  17589  mreexdomd  17591  rescabs  17776  rescabs2  17777  resssetc  18035  resscatc  18052  estrres  18081  yonedalem1  18214  yonedalem21  18215  yonedalem3a  18216  yonedalem4c  18219  yonedalem22  18220  yonedalem3b  18221  yonedainv  18223  yonffthlem  18224  joinfval  18313  meetfval  18327  acsdomd  18499  ressmulgnnd  18993  gass  19216  pmtrfconj  19381  sylow2blem2  19536  dprdres  19945  dmdprdsplitlem  19954  primefld  20726  pwssplit0  20998  pwssplit1  20999  pwssplit2  21000  pwssplit3  21001  frlmsplit2  21716  frlmsslss  21717  opsrtoslem2  21997  evlsgsumadd  22032  evlsgsummul  22033  evls1gsumadd  22245  evls1gsummul  22246  evl1gsummul  22281  neiptoptop  23052  lpval  23060  neitr  23101  ordtbaslem  23109  ordtrest2  23125  cnrest2  23207  cnpresti  23209  cnprest  23210  cnprest2  23211  connsuba  23341  connsubclo  23345  unconn  23350  1stcelcls  23382  hausmapdom  23421  dissnref  23449  ptbasfi  23502  ptcls  23537  cnmpt2res  23598  qtopval2  23617  elqtop  23618  qtoprest  23638  ptuncnv  23728  ptunhmeo  23729  fsubbas  23788  elfm  23868  rnelfmlem  23873  rnelfm  23874  fmfnfmlem4  23878  flimclslem  23905  hauspwpwdom  23909  ptcmplem1  23973  cnextcn  23988  cnextfres1  23989  isust  24125  trust  24151  elutop  24155  restutop  24159  trcfilu  24215  cfiluweak  24216  psmetres2  24236  xmetres2  24283  fmcfil  25206  dvaddf  25879  dvmulf  25880  dvcmulf  25882  dvcof  25886  ulmss  26340  nosupno  27649  noinfno  27664  sssslt1  27742  sssslt2  27743  sltonex  28204  perpln1  28691  perpln2  28692  isperp  28693  wksfval  29591  fnpreimac  32646  fisuppov1  32657  resf1o  32704  hashpss  32785  gsumpart  33041  gsumwrd2dccat  33051  cycpmco2lem5  33103  elrgspnlem1  33210  elrgspnlem2  33211  elrgspnlem3  33212  elrgspnlem4  33213  elrgspn  33214  erlval  33226  rlocval  33227  rlocbas  33235  fldgenval  33279  islinds5  33332  ellspds  33333  elrsp  33337  elrspunidl  33393  resssra  33577  lbslelsp  33587  lbsdiflsp0  33616  irngval  33674  ordtrest2NEW  33907  lmlim  33931  esummono  34038  esumrnmpt2  34052  esumpinfval  34057  elcarsg  34290  carsgmon  34299  carsggect  34303  reprval  34595  repr0  34596  reprsuc  34600  reprss  34602  reprinrn  34603  reprlt  34604  reprgt  34606  reprinfz1  34607  reprpmtf1o  34611  reprdifc  34612  bnj1413  35019  cvmliftmolem1  35262  satf0suclem  35356  fwddifval  36144  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  42109  sticksstones20  42148  aks6d1c6lem3  42154  psrbagres  42528  selvcllemh  42562  selvcllem4  42563  selvcllem5  42564  selvcl  42565  selvval2  42566  selvvvval  42567  evlselv  42569  selvadd  42570  selvmul  42571  fsuppssindlem2  42574  fsuppssind  42575  elrfi  42676  elrfirn2  42678  oaun3lem3  43359  nadd2rabex  43369  clcnvlem  43606  relexpss1d  43688  k0004lem2  44131  ixpssmapc  45061  restuni4  45109  restsubel  45141  wessf1ornlem  45173  disjinfi  45180  unirnmap  45196  inmap  45197  difmapsn  45200  unirnmapsn  45202  ssmapsn  45204  limsupre  45633  limsuppnfdlem  45693  limsuppnflem  45702  limsupmnflem  45712  limsupre2lem  45716  liminfval4  45781  liminfval3  45782  icccncfext  45879  dvdivcncf  45919  dvnprodlem1  45938  dvnprodlem2  45939  ovolsplit  45980  stoweidlem31  46023  stoweidlem53  46045  stoweidlem57  46049  stoweidlem59  46051  etransclem46  46272  salexct  46326  subsaluni  46352  fsumlesge0  46369  sge0iunmptlemfi  46405  sge0iunmptlemre  46407  meadjuni  46449  meadjiunlem  46457  omessle  46490  omecl  46495  isomenndlem  46522  caragencmpl  46527  ovnval2  46537  ovnval2b  46544  ovncvrrp  46556  ovncl  46559  hoidmvlelem2  46588  hoidmvlelem3  46589  ovncvr2  46603  ovnsubadd2lem  46637  ovnovollem3  46650  vonvolmbllem  46652  vonvolmbl  46653  sssmf  46730  incsmf  46734  issmflelem  46736  issmfle  46737  smfconst  46741  issmfgtlem  46747  issmfgt  46748  smfaddlem2  46756  decsmf  46759  issmfgelem  46761  issmfge  46762  nsssmfmbflem  46770  smfpimioo  46779  smfresal  46780  smfmullem4  46786  smfpimbor1lem1  46790  smf2id  46793  upwlksfval  48117  toplatglb  48983