Theorem ssexd 4733

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

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  sselpwd  4734  opabbrex  6593  opabex2  6997  soex  7002  fex2  7014  fnwelem  7179  fnse  7181  extmptsuppeq  7206  f1imaen2g  7903  ordtypelem10  8315  oismo  8328  wofib  8333  wemapso  8339  wdom2d  8368  wdomd  8369  unxpwdom2  8376  cantnfle  8451  cantnflt  8452  cantnflt2  8453  cantnfp1lem2  8459  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cnfcomlem  8479  cnfcom  8480  cnfcom2lem  8481  cnfcom3lem  8483  acni2  8752  fin1a2lem12  9116  hsmexlem1  9131  zorn2lem4  9204  fpwwe2lem2  9333  fpwwe2lem5  9335  fpwwe2lem12  9342  fpwwe2  9344  fpwwelem  9346  canthwelem  9351  pwfseqlem4  9363  trclfv  13589  hashbcss  15546  strssd  15737  restid2  15914  divsfval  16030  mrieqv2d  16122  mrissmrcd  16123  mreexexlemd  16127  mreexexlem3d  16129  mreexexlem4d  16130  mreexexdOLD  16132  mreexdomd  16133  rescabs  16316  rescabs2  16317  resssetc  16565  resscatc  16578  estrres  16602  yonedalem1  16735  yonedalem21  16736  yonedalem3a  16737  yonedalem4c  16740  yonedalem22  16741  yonedalem3b  16742  yonedainv  16744  yonffthlem  16745  joinfval  16824  meetfval  16838  acsdomd  17004  gass  17557  pmtrfconj  17709  sylow2blem2  17859  dprdres  18250  dmdprdsplitlem  18259  pwssplit0  18879  pwssplit1  18880  pwssplit2  18881  pwssplit3  18882  opsrtoslem2  19306  evls1gsumadd  19510  evls1gsummul  19511  evl1gsummul  19545  frlmsplit2  19931  frlmsslss  19932  neiptoptop  20745  lpval  20753  neitr  20794  ordtbaslem  20802  ordtrest2  20818  cnrest2  20900  cnpresti  20902  cnprest  20903  cnprest2  20904  consuba  21033  consubclo  21037  uncon  21042  1stcelcls  21074  hausmapdom  21113  dissnref  21141  ptbasfi  21194  ptcls  21229  cnmpt2res  21290  qtopval2  21309  elqtop  21310  qtoprest  21330  ptuncnv  21420  ptunhmeo  21421  fsubbas  21481  elfm  21561  rnelfmlem  21566  rnelfm  21567  fmfnfmlem4  21571  flimclslem  21598  hauspwpwdom  21602  ptcmplem1  21666  cnextcn  21681  cnextfres1  21682  isust  21817  trust  21843  elutop  21847  restutop  21851  trcfilu  21908  cfiluweak  21909  psmetres2  21929  xmetres2  21976  fmcfil  22878  dvnf  23496  dvnbss  23497  dvaddf  23511  dvmulf  23512  dvcmulf  23514  dvcof  23517  ulmss  23955  perpln1  25405  perpln2  25406  isperp  25407  wlks  26047  trls  26066  resf1o  28893  crefi  29242  ordtrest2NEW  29297  lmlim  29321  esummono  29443  esumrnmpt2  29457  esumpinfval  29462  carsgmon  29703  carsggect  29707  bnj1413  30357  cvmliftmolem1  30517  fwddifval  31439  neibastop1  31524  neibastop2lem  31525  fnejoin1  31533  filnetlem3  31545  filnetlem4  31546  dissneqlem  32363  elrfi  36275  elrfirn2  36277  clcnvlem  36949  relexpss1d  37016  k0004lem2  37466  ixpssmapc  38269  restuni4  38336  wessf1ornlem  38366  unirnmap  38395  inmap  38396  difmapsn  38399  unirnmapsn  38401  ssmapsn  38403  limsupre  38708  icccncfext  38773  dvdivcncf  38817  dvnprodlem1  38836  dvnprodlem2  38837  ovolsplit  38881  stoweidlem31  38924  stoweidlem53  38946  stoweidlem57  38950  stoweidlem59  38952  etransclem46  39173  saliuncl  39218  salexct  39228  subsaluni  39254  fsumlesge0  39270  sge0f1o  39275  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  meadjuni  39350  meadjiunlem  39358  omessle  39388  omecl  39393  isomenndlem  39420  caragencmpl  39425  ovnval2  39435  ovnval2b  39442  ovncvrrp  39454  ovncl  39457  hoidmvlelem2  39486  hoidmvlelem3  39487  ovncvr2  39501  ovnsubadd2lem  39535  ovnovollem3  39548  vonvolmbllem  39550  vonvolmbl  39551  issmfltle  39622  sssmf  39625  incsmf  39629  issmflelem  39631  issmfle  39632  smfconst  39636  issmfgtlem  39642  issmfgt  39643  smfaddlem2  39650  decsmf  39653  issmfgelem  39655  issmfge  39656  nsssmfmbflem  39664  smfpimioo  39672  smfresal  39673  smfmullem4  39679  smfpimbor1lem1  39683  smf2id  39686  1wlksfval  40811  wlksfval  40812