Theorem ssexd 5263

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903

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 5235

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 3395  df-v 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  abexd  5264  sselpwd  5267  opabbrex  7402  soex  7854  fex2  7869  fabexd  7870  mapex  7874  funexw  7887  opabex2  7992  fnwelem  8064  fnse  8066  extmptsuppeq  8121  f1setex  8784  f1imaen2g  8940  fsuppss  9273  ordtypelem10  9419  oismo  9432  wofib  9437  wdom2d  9472  wdomd  9473  unxpwdom2  9480  ttrclexg  9619  djuexALT  9818  acni2  9940  fin1a2lem12  10305  hsmexlem1  10320  zorn2lem4  10393  fpwwe2lem2  10526  fpwwe2lem4  10528  fpwwe2lem11  10535  fpwwe2  10537  fpwwelem  10539  canthwelem  10544  pwfseqlem4  10556  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  18957  gass  19180  pmtrfconj  19345  sylow2blem2  19500  dprdres  19909  dmdprdsplitlem  19918  primefld  20690  pwssplit0  20962  pwssplit1  20963  pwssplit2  20964  pwssplit3  20965  frlmsplit2  21680  frlmsslss  21681  opsrtoslem2  21961  evlsgsumadd  21996  evlsgsummul  21997  evls1gsumadd  22209  evls1gsummul  22210  evl1gsummul  22245  neiptoptop  23016  lpval  23024  neitr  23065  ordtbaslem  23073  ordtrest2  23089  cnrest2  23171  cnpresti  23173  cnprest  23174  cnprest2  23175  connsuba  23305  connsubclo  23309  unconn  23314  1stcelcls  23346  hausmapdom  23385  dissnref  23413  ptbasfi  23466  ptcls  23501  cnmpt2res  23562  qtopval2  23581  elqtop  23582  qtoprest  23602  ptuncnv  23692  ptunhmeo  23693  fsubbas  23752  elfm  23832  rnelfmlem  23837  rnelfm  23838  fmfnfmlem4  23842  flimclslem  23869  hauspwpwdom  23873  ptcmplem1  23937  cnextcn  23952  cnextfres1  23953  isust  24089  trust  24115  elutop  24119  restutop  24123  trcfilu  24179  cfiluweak  24180  psmetres2  24200  xmetres2  24247  fmcfil  25170  dvaddf  25843  dvmulf  25844  dvcmulf  25846  dvcof  25850  ulmss  26304  nosupno  27613  noinfno  27628  sssslt1  27707  sssslt2  27708  sltonex  28170  perpln1  28659  perpln2  28660  isperp  28661  wksfval  29559  fnpreimac  32622  fisuppov1  32633  resf1o  32682  hashpss  32763  gsumpart  33019  gsumwrd2dccat  33029  cycpmco2lem5  33081  elrgspnlem1  33191  elrgspnlem2  33192  elrgspnlem3  33193  elrgspnlem4  33194  elrgspn  33195  erlval  33207  rlocval  33208  rlocbas  33216  fldgenval  33260  islinds5  33313  ellspds  33314  elrsp  33318  elrspunidl  33374  resssra  33569  lbslelsp  33580  lbsdiflsp0  33609  irngval  33668  ordtrest2NEW  33906  lmlim  33930  esummono  34037  esumrnmpt2  34051  esumpinfval  34056  elcarsg  34289  carsgmon  34298  carsggect  34302  reprval  34594  repr0  34595  reprsuc  34599  reprss  34601  reprinrn  34602  reprlt  34603  reprgt  34605  reprinfz1  34606  reprpmtf1o  34610  reprdifc  34611  bnj1413  35018  cvmliftmolem1  35274  satf0suclem  35368  fwddifval  36156  neibastop1  36353  neibastop2lem  36354  fnejoin1  36362  filnetlem3  36374  filnetlem4  36375  weiunse  36462  numiunnum  36464  bj-imdirval2lem  37176  bj-imdirval3  37178  bj-imdirco  37184  dissneqlem  37334  aks6d1c2lem4  42120  sticksstones20  42159  aks6d1c6lem3  42165  psrbagres  42539  selvcllemh  42573  selvcllem4  42574  selvcllem5  42575  selvcl  42576  selvval2  42577  selvvvval  42578  evlselv  42580  selvadd  42581  selvmul  42582  fsuppssindlem2  42585  fsuppssind  42586  elrfi  42687  elrfirn2  42689  oaun3lem3  43369  nadd2rabex  43379  clcnvlem  43616  relexpss1d  43698  k0004lem2  44141  ixpssmapc  45071  restuni4  45119  restsubel  45151  wessf1ornlem  45183  disjinfi  45190  unirnmap  45206  inmap  45207  difmapsn  45210  unirnmapsn  45212  ssmapsn  45214  limsupre  45642  limsuppnfdlem  45702  limsuppnflem  45711  limsupmnflem  45721  limsupre2lem  45725  liminfval4  45790  liminfval3  45791  icccncfext  45888  dvdivcncf  45928  dvnprodlem1  45947  dvnprodlem2  45948  ovolsplit  45989  stoweidlem31  46032  stoweidlem53  46054  stoweidlem57  46058  stoweidlem59  46060  etransclem46  46281  salexct  46335  subsaluni  46361  fsumlesge0  46378  sge0iunmptlemfi  46414  sge0iunmptlemre  46416  meadjuni  46458  meadjiunlem  46466  omessle  46499  omecl  46504  isomenndlem  46531  caragencmpl  46536  ovnval2  46546  ovnval2b  46553  ovncvrrp  46565  ovncl  46568  hoidmvlelem2  46597  hoidmvlelem3  46598  ovncvr2  46612  ovnsubadd2lem  46646  ovnovollem3  46659  vonvolmbllem  46661  vonvolmbl  46662  sssmf  46739  incsmf  46743  issmflelem  46745  issmfle  46746  smfconst  46750  issmfgtlem  46756  issmfgt  46757  smfaddlem2  46765  decsmf  46768  issmfgelem  46770  issmfge  46771  nsssmfmbflem  46779  smfpimioo  46788  smfresal  46789  smfmullem4  46795  smfpimbor1lem1  46799  smf2id  46802  upwlksfval  48139  toplatglb  49005