Theorem ssexd 5255

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

Syntax hints:   → wi 4   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-in 3892  df-ss 3902

This theorem is referenced by:  abexd  5256  sselpwd  5259  moabex  5400  opabbrex  7413  soex  7865  fex2  7880  fabexd  7881  mapex  7885  funexw  7898  opabex2  8003  fnwelem  8075  fnse  8077  extmptsuppeq  8132  f1setex  8798  f1imaen2g  8956  fsuppss  9290  ordtypelem10  9436  oismo  9449  wofib  9454  wdom2d  9489  wdomd  9490  unxpwdom2  9497  ttrclexg  9639  djuexALT  9841  acni2  9963  fin1a2lem12  10328  hsmexlem1  10343  zorn2lem4  10416  ondomon  10480  fpwwe2lem2  10550  fpwwe2lem4  10552  fpwwe2lem11  10559  fpwwe2  10561  fpwwelem  10563  canthwelem  10568  pwfseqlem4  10580  hashf1lem1  14412  trclfv  14957  hashbcss  16970  strssd  17170  restid2  17388  divsfval  17506  mrieqv2d  17600  mrissmrcd  17601  mreexexlemd  17605  mreexexlem3d  17607  mreexexlem4d  17608  mreexdomd  17610  rescabs  17795  rescabs2  17796  resssetc  18054  resscatc  18071  estrres  18100  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedainv  18242  yonffthlem  18243  joinfval  18332  meetfval  18346  acsdomd  18518  ressmulgnnd  19049  gass  19271  pmtrfconj  19436  sylow2blem2  19591  dprdres  20000  dmdprdsplitlem  20009  primefld  20781  pwssplit0  21052  pwssplit1  21053  pwssplit2  21054  pwssplit3  21055  frlmsplit2  21752  frlmsslss  21753  psrbagres  21909  opsrtoslem2  22036  evlsgsumadd  22076  evlsgsummul  22077  selvcllemh  22117  selvcllem4  22118  selvcllem5  22119  selvcl  22120  selvval2  22121  selvvvval  22122  selvadd  22123  selvmul  22124  evls1gsumadd  22314  evls1gsummul  22315  evl1gsummul  22350  neiptoptop  23118  lpval  23126  neitr  23167  ordtbaslem  23175  ordtrest2  23191  cnrest2  23273  cnpresti  23275  cnprest  23276  cnprest2  23277  connsuba  23407  connsubclo  23411  unconn  23416  1stcelcls  23448  hausmapdom  23487  dissnref  23515  ptbasfi  23568  ptcls  23603  cnmpt2res  23664  qtopval2  23683  elqtop  23684  qtoprest  23704  ptuncnv  23794  ptunhmeo  23795  fsubbas  23854  elfm  23934  rnelfmlem  23939  rnelfm  23940  fmfnfmlem4  23944  flimclslem  23971  hauspwpwdom  23975  ptcmplem1  24039  cnextcn  24054  cnextfres1  24055  isust  24191  trust  24216  elutop  24220  restutop  24224  trcfilu  24280  cfiluweak  24281  psmetres2  24301  xmetres2  24348  fmcfil  25261  dvaddf  25931  dvmulf  25932  dvcmulf  25934  dvcof  25937  ulmss  26384  nosupno  27689  noinfno  27704  ssslts1  27787  ssslts2  27788  ltonsex  28276  perpln1  28800  perpln2  28801  isperp  28802  wksfval  29700  fnpreimac  32766  fisuppov1  32779  resf1o  32826  hashpss  32905  gsumpart  33148  gsumwrd2dccat  33163  cycpmco2lem5  33215  elrgspnlem1  33327  elrgspnlem2  33328  elrgspnlem3  33329  elrgspnlem4  33330  elrgspn  33331  erlval  33343  rlocval  33344  rlocbas  33352  fldgenval  33400  islinds5  33454  ellspds  33455  elrsp  33459  elrspunidl  33515  mplasclco  33712  selvascl  33713  evlextv  33738  psrmonprod  33748  esplympl  33763  esplyind  33771  resssra  33783  lbslelsp  33794  lbsdiflsp0  33822  irngval  33881  ordtrest2NEW  34119  lmlim  34143  esummono  34250  esumrnmpt2  34264  esumpinfval  34269  elcarsg  34501  carsgmon  34510  carsggect  34514  reprval  34806  repr0  34807  reprsuc  34811  reprss  34813  reprinrn  34814  reprlt  34815  reprgt  34817  reprinfz1  34818  reprpmtf1o  34822  reprdifc  34823  bnj1413  35232  cvmliftmolem1  35524  satf0suclem  35618  fwddifval  36405  neibastop1  36602  neibastop2lem  36603  fnejoin1  36611  filnetlem3  36623  filnetlem4  36624  weiunse  36711  numiunnum  36713  bj-imdirval2lem  37557  bj-imdirval3  37559  bj-imdirco  37565  dissneqlem  37717  aks6d1c2lem4  42627  sticksstones20  42666  aks6d1c6lem3  42672  evlselv  43054  fsuppssindlem2  43057  fsuppssind  43058  elrfi  43158  elrfirn2  43160  oaun3lem3  43836  nadd2rabex  43846  clcnvlem  44082  relexpss1d  44164  k0004lem2  44607  ixpssmapc  45536  restuni4  45582  restsubel  45614  wessf1ornlem  45646  disjinfi  45653  unirnmap  45667  inmap  45668  difmapsn  45671  unirnmapsn  45673  ssmapsn  45675  limsupre  46098  limsuppnfdlem  46158  limsuppnflem  46167  limsupmnflem  46177  limsupre2lem  46181  liminfval4  46246  liminfval3  46247  icccncfext  46344  dvdivcncf  46384  dvnprodlem1  46403  dvnprodlem2  46404  ovolsplit  46445  stoweidlem31  46488  stoweidlem53  46510  stoweidlem57  46514  stoweidlem59  46516  etransclem46  46737  salexct  46791  subsaluni  46817  fsumlesge0  46834  sge0iunmptlemfi  46870  sge0iunmptlemre  46872  meadjuni  46914  meadjiunlem  46922  omessle  46955  omecl  46960  isomenndlem  46987  caragencmpl  46992  ovnval2  47002  ovnval2b  47009  ovncvrrp  47021  ovncl  47024  hoidmvlelem2  47053  hoidmvlelem3  47054  ovncvr2  47068  ovnsubadd2lem  47102  ovnovollem3  47115  vonvolmbllem  47117  vonvolmbl  47118  sssmf  47195  incsmf  47199  issmflelem  47201  issmfle  47202  smfconst  47206  issmfgtlem  47212  issmfgt  47213  smfaddlem2  47221  decsmf  47224  issmfgelem  47226  issmfge  47227  nsssmfmbflem  47235  smfpimioo  47244  smfresal  47245  smfmullem4  47251  smfpimbor1lem1  47255  smf2id  47258  upwlksfval  48640  toplatglb  49505