Theorem ssexd 5318

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

Syntax hints:   → wi 4   ∈ wcel 2099  Vcvv 3469   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  abexd  5319  sselpwd  5322  opabbrex  7465  soex  7923  fex2  7935  funexw  7949  opabex2  8055  fnwelem  8130  fnse  8132  extmptsuppeq  8186  f1setex  8869  f1imaen2g  9029  fsuppss  9400  ordtypelem10  9544  oismo  9557  wofib  9562  wdom2d  9597  wdomd  9598  unxpwdom2  9605  ttrclexg  9740  djuexALT  9939  acni2  10063  fin1a2lem12  10428  hsmexlem1  10443  zorn2lem4  10516  fpwwe2lem2  10649  fpwwe2lem4  10651  fpwwe2lem11  10658  fpwwe2  10660  fpwwelem  10662  canthwelem  10667  pwfseqlem4  10679  hashf1lem1  14441  trclfv  14973  hashbcss  16966  strssd  17168  restid2  17405  divsfval  17522  mrieqv2d  17612  mrissmrcd  17613  mreexexlemd  17617  mreexexlem3d  17619  mreexexlem4d  17620  mreexdomd  17622  rescabs  17811  rescabsOLD  17812  rescabs2  17813  resssetc  18074  resscatc  18091  estrres  18123  yonedalem1  18257  yonedalem21  18258  yonedalem3a  18259  yonedalem4c  18262  yonedalem22  18263  yonedalem3b  18264  yonedainv  18266  yonffthlem  18267  joinfval  18358  meetfval  18372  acsdomd  18542  gass  19245  permsetexOLD  19317  pmtrfconj  19414  sylow2blem2  19569  dprdres  19978  dmdprdsplitlem  19987  primefld  20686  pwssplit0  20936  pwssplit1  20937  pwssplit2  20938  pwssplit3  20939  frlmsplit2  21700  frlmsslss  21701  opsrtoslem2  21993  evlsgsumadd  22030  evlsgsummul  22031  evls1gsumadd  22236  evls1gsummul  22237  evl1gsummul  22272  neiptoptop  23028  lpval  23036  neitr  23077  ordtbaslem  23085  ordtrest2  23101  cnrest2  23183  cnpresti  23185  cnprest  23186  cnprest2  23187  connsuba  23317  connsubclo  23321  unconn  23326  1stcelcls  23358  hausmapdom  23397  dissnref  23425  ptbasfi  23478  ptcls  23513  cnmpt2res  23574  qtopval2  23593  elqtop  23594  qtoprest  23614  ptuncnv  23704  ptunhmeo  23705  fsubbas  23764  elfm  23844  rnelfmlem  23849  rnelfm  23850  fmfnfmlem4  23854  flimclslem  23881  hauspwpwdom  23885  ptcmplem1  23949  cnextcn  23964  cnextfres1  23965  isust  24101  trust  24127  elutop  24131  restutop  24135  trcfilu  24192  cfiluweak  24193  psmetres2  24213  xmetres2  24260  fmcfil  25193  dvaddf  25866  dvmulf  25867  dvcmulf  25869  dvcof  25873  ulmss  26326  nosupno  27629  noinfno  27644  sssslt1  27721  sssslt2  27722  sltonex  28147  perpln1  28507  perpln2  28508  isperp  28509  wksfval  29416  fnpreimac  32450  resf1o  32506  gsumpart  32763  cycpmco2lem5  32845  erlval  32966  rlocval  32967  rlocbas  32975  fldgenval  32993  islinds5  33073  ellspds  33074  elrsp  33079  elrspunidl  33133  resssra  33273  lbsdiflsp0  33310  irngval  33349  ordtrest2NEW  33514  lmlim  33538  esummono  33663  esumrnmpt2  33677  esumpinfval  33682  elcarsg  33915  carsgmon  33924  carsggect  33928  reprval  34232  repr0  34233  reprsuc  34237  reprss  34239  reprinrn  34240  reprlt  34241  reprgt  34243  reprinfz1  34244  reprpmtf1o  34248  reprdifc  34249  bnj1413  34656  cvmliftmolem1  34881  satf0suclem  34975  fwddifval  35748  neibastop1  35833  neibastop2lem  35834  fnejoin1  35842  filnetlem3  35854  filnetlem4  35855  bj-imdirval2lem  36651  bj-imdirval3  36653  bj-imdirco  36659  dissneqlem  36809  aks6d1c2lem4  41582  sticksstones20  41622  aks6d1c6lem3  41628  psrbagres  41748  selvcllemh  41785  selvcllem4  41786  selvcllem5  41787  selvcl  41788  selvval2  41789  selvvvval  41790  evlselv  41792  selvadd  41793  selvmul  41794  fsuppssindlem2  41797  fsuppssind  41798  elrfi  42086  elrfirn2  42088  oaun3lem3  42777  nadd2rabex  42787  clcnvlem  43025  relexpss1d  43107  k0004lem2  43550  ixpssmapc  44410  restuni4  44459  restsubel  44496  wessf1ornlem  44530  disjinfi  44537  unirnmap  44553  inmap  44554  difmapsn  44557  unirnmapsn  44559  ssmapsn  44561  limsupre  45001  limsuppnfdlem  45061  limsuppnflem  45070  limsupmnflem  45080  limsupre2lem  45084  liminfval4  45149  liminfval3  45150  icccncfext  45247  dvdivcncf  45287  dvnprodlem1  45306  dvnprodlem2  45307  ovolsplit  45348  stoweidlem31  45391  stoweidlem53  45413  stoweidlem57  45417  stoweidlem59  45419  etransclem46  45640  salexct  45694  subsaluni  45720  fsumlesge0  45737  sge0f1o  45742  sge0iunmptlemfi  45773  sge0iunmptlemre  45775  meadjuni  45817  meadjiunlem  45825  omessle  45858  omecl  45863  isomenndlem  45890  caragencmpl  45895  ovnval2  45905  ovnval2b  45912  ovncvrrp  45924  ovncl  45927  hoidmvlelem2  45956  hoidmvlelem3  45957  ovncvr2  45971  ovnsubadd2lem  46005  ovnovollem3  46018  vonvolmbllem  46020  vonvolmbl  46021  sssmf  46098  incsmf  46102  issmflelem  46104  issmfle  46105  smfconst  46109  issmfgtlem  46115  issmfgt  46116  smfaddlem2  46124  decsmf  46127  issmfgelem  46129  issmfge  46130  nsssmfmbflem  46138  smfpimioo  46147  smfresal  46148  smfmullem4  46154  smfpimbor1lem1  46158  smf2id  46161  upwlksfval  47169  toplatglb  47984