Theorem ssexd 5254

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3427   ⊆ wss 3885

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 2707  ax-sep 5220

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-in 3892  df-ss 3902

This theorem is referenced by:  abexd  5255  sselpwd  5258  moabex  5399  opabbrex  7409  soex  7861  fex2  7876  fabexd  7877  mapex  7881  funexw  7894  opabex2  7999  fnwelem  8070  fnse  8072  extmptsuppeq  8127  f1setex  8793  f1imaen2g  8951  fsuppss  9285  ordtypelem10  9431  oismo  9444  wofib  9449  wdom2d  9484  wdomd  9485  unxpwdom2  9492  ttrclexg  9633  djuexALT  9835  acni2  9957  fin1a2lem12  10322  hsmexlem1  10337  zorn2lem4  10410  ondomon  10474  fpwwe2lem2  10544  fpwwe2lem4  10546  fpwwe2lem11  10553  fpwwe2  10555  fpwwelem  10557  canthwelem  10562  pwfseqlem4  10574  hashf1lem1  14406  trclfv  14951  hashbcss  16964  strssd  17164  restid2  17382  divsfval  17500  mrieqv2d  17594  mrissmrcd  17595  mreexexlemd  17599  mreexexlem3d  17601  mreexexlem4d  17602  mreexdomd  17604  rescabs  17789  rescabs2  17790  resssetc  18048  resscatc  18065  estrres  18094  yonedalem1  18227  yonedalem21  18228  yonedalem3a  18229  yonedalem4c  18232  yonedalem22  18233  yonedalem3b  18234  yonedainv  18236  yonffthlem  18237  joinfval  18326  meetfval  18340  acsdomd  18512  ressmulgnnd  19043  gass  19265  pmtrfconj  19430  sylow2blem2  19585  dprdres  19994  dmdprdsplitlem  20003  primefld  20771  pwssplit0  21042  pwssplit1  21043  pwssplit2  21044  pwssplit3  21045  frlmsplit2  21742  frlmsslss  21743  opsrtoslem2  22023  evlsgsumadd  22063  evlsgsummul  22064  evls1gsumadd  22277  evls1gsummul  22278  evl1gsummul  22313  neiptoptop  23084  lpval  23092  neitr  23133  ordtbaslem  23141  ordtrest2  23157  cnrest2  23239  cnpresti  23241  cnprest  23242  cnprest2  23243  connsuba  23373  connsubclo  23377  unconn  23382  1stcelcls  23414  hausmapdom  23453  dissnref  23481  ptbasfi  23534  ptcls  23569  cnmpt2res  23630  qtopval2  23649  elqtop  23650  qtoprest  23670  ptuncnv  23760  ptunhmeo  23761  fsubbas  23820  elfm  23900  rnelfmlem  23905  rnelfm  23906  fmfnfmlem4  23910  flimclslem  23937  hauspwpwdom  23941  ptcmplem1  24005  cnextcn  24020  cnextfres1  24021  isust  24157  trust  24182  elutop  24186  restutop  24190  trcfilu  24246  cfiluweak  24247  psmetres2  24267  xmetres2  24314  fmcfil  25227  dvaddf  25897  dvmulf  25898  dvcmulf  25900  dvcof  25903  ulmss  26350  nosupno  27655  noinfno  27670  ssslts1  27753  ssslts2  27754  ltonsex  28242  perpln1  28766  perpln2  28767  isperp  28768  wksfval  29666  fnpreimac  32731  fisuppov1  32744  resf1o  32791  hashpss  32870  gsumpart  33112  gsumwrd2dccat  33127  cycpmco2lem5  33179  elrgspnlem1  33291  elrgspnlem2  33292  elrgspnlem3  33293  elrgspnlem4  33294  elrgspn  33295  erlval  33307  rlocval  33308  rlocbas  33316  fldgenval  33361  islinds5  33415  ellspds  33416  elrsp  33420  elrspunidl  33476  evlextv  33674  psrmonprod  33684  esplympl  33699  esplyind  33707  resssra  33719  lbslelsp  33730  lbsdiflsp0  33758  irngval  33817  ordtrest2NEW  34055  lmlim  34079  esummono  34186  esumrnmpt2  34200  esumpinfval  34205  elcarsg  34437  carsgmon  34446  carsggect  34450  reprval  34742  repr0  34743  reprsuc  34747  reprss  34749  reprinrn  34750  reprlt  34751  reprgt  34753  reprinfz1  34754  reprpmtf1o  34758  reprdifc  34759  bnj1413  35165  cvmliftmolem1  35451  satf0suclem  35545  fwddifval  36332  neibastop1  36529  neibastop2lem  36530  fnejoin1  36538  filnetlem3  36550  filnetlem4  36551  weiunse  36638  numiunnum  36640  bj-imdirval2lem  37484  bj-imdirval3  37486  bj-imdirco  37492  dissneqlem  37644  aks6d1c2lem4  42554  sticksstones20  42593  aks6d1c6lem3  42599  psrbagres  42977  selvcllemh  43001  selvcllem4  43002  selvcllem5  43003  selvcl  43004  selvval2  43005  selvvvval  43006  evlselv  43008  selvadd  43009  selvmul  43010  fsuppssindlem2  43013  fsuppssind  43014  elrfi  43114  elrfirn2  43116  oaun3lem3  43792  nadd2rabex  43802  clcnvlem  44038  relexpss1d  44120  k0004lem2  44563  ixpssmapc  45492  restuni4  45539  restsubel  45571  wessf1ornlem  45603  disjinfi  45610  unirnmap  45625  inmap  45626  difmapsn  45629  unirnmapsn  45631  ssmapsn  45633  limsupre  46057  limsuppnfdlem  46117  limsuppnflem  46126  limsupmnflem  46136  limsupre2lem  46140  liminfval4  46205  liminfval3  46206  icccncfext  46303  dvdivcncf  46343  dvnprodlem1  46362  dvnprodlem2  46363  ovolsplit  46404  stoweidlem31  46447  stoweidlem53  46469  stoweidlem57  46473  stoweidlem59  46475  etransclem46  46696  salexct  46750  subsaluni  46776  fsumlesge0  46793  sge0iunmptlemfi  46829  sge0iunmptlemre  46831  meadjuni  46873  meadjiunlem  46881  omessle  46914  omecl  46919  isomenndlem  46946  caragencmpl  46951  ovnval2  46961  ovnval2b  46968  ovncvrrp  46980  ovncl  46983  hoidmvlelem2  47012  hoidmvlelem3  47013  ovncvr2  47027  ovnsubadd2lem  47061  ovnovollem3  47074  vonvolmbllem  47076  vonvolmbl  47077  sssmf  47154  incsmf  47158  issmflelem  47160  issmfle  47161  smfconst  47165  issmfgtlem  47171  issmfgt  47172  smfaddlem2  47180  decsmf  47183  issmfgelem  47185  issmfge  47186  nsssmfmbflem  47194  smfpimioo  47203  smfresal  47204  smfmullem4  47210  smfpimbor1lem1  47214  smf2id  47217  upwlksfval  48599  toplatglb  49464