Theorem ssexd 5227

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3494   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  sselpwd  5229  opabbrex  7206  soex  7625  fex2  7637  funexw  7652  opabex2  7754  fnwelem  7824  fnse  7826  extmptsuppeq  7853  f1imaen2g  8569  ordtypelem10  8990  oismo  9003  wofib  9008  wemapso  9014  wdom2d  9043  wdomd  9044  unxpwdom2  9051  djuexALT  9350  acni2  9471  fin1a2lem12  9832  hsmexlem1  9847  zorn2lem4  9920  fpwwe2lem2  10053  fpwwe2lem5  10055  fpwwe2lem12  10062  fpwwe2  10064  fpwwelem  10066  canthwelem  10071  pwfseqlem4  10083  trclfv  14359  hashbcss  16339  strssd  16532  restid2  16703  divsfval  16819  mrieqv2d  16909  mrissmrcd  16910  mreexexlemd  16914  mreexexlem3d  16916  mreexexlem4d  16917  mreexdomd  16919  rescabs  17102  rescabs2  17103  resssetc  17351  resscatc  17364  estrres  17388  yonedalem1  17521  yonedalem21  17522  yonedalem3a  17523  yonedalem4c  17526  yonedalem22  17527  yonedalem3b  17528  yonedainv  17530  yonffthlem  17531  joinfval  17610  meetfval  17624  acsdomd  17790  gass  18430  permsetex  18497  pmtrfconj  18593  sylow2blem2  18745  dprdres  19149  dmdprdsplitlem  19158  primefld  19583  pwssplit0  19829  pwssplit1  19830  pwssplit2  19831  pwssplit3  19832  opsrtoslem2  20264  evlsgsumadd  20303  evlsgsummul  20304  evls1gsumadd  20486  evls1gsummul  20487  evl1gsummul  20522  frlmsplit2  20916  frlmsslss  20917  neiptoptop  21738  lpval  21746  neitr  21787  ordtbaslem  21795  ordtrest2  21811  cnrest2  21893  cnpresti  21895  cnprest  21896  cnprest2  21897  connsuba  22027  connsubclo  22031  unconn  22036  1stcelcls  22068  hausmapdom  22107  dissnref  22135  ptbasfi  22188  ptcls  22223  cnmpt2res  22284  qtopval2  22303  elqtop  22304  qtoprest  22324  ptuncnv  22414  ptunhmeo  22415  fsubbas  22474  elfm  22554  rnelfmlem  22559  rnelfm  22560  fmfnfmlem4  22564  flimclslem  22591  hauspwpwdom  22595  ptcmplem1  22659  cnextcn  22674  cnextfres1  22675  isust  22811  trust  22837  elutop  22841  restutop  22845  trcfilu  22902  cfiluweak  22903  psmetres2  22923  xmetres2  22970  fmcfil  23874  dvaddf  24538  dvmulf  24539  dvcmulf  24541  dvcof  24544  ulmss  24984  perpln1  26495  perpln2  26496  isperp  26497  wksfval  27390  fnpreimac  30415  resf1o  30465  cycpmco2lem5  30772  islinds5  30932  ellspds  30933  lbsdiflsp0  31022  ordtrest2NEW  31166  lmlim  31190  esummono  31313  esumrnmpt2  31327  esumpinfval  31332  elcarsg  31563  carsgmon  31572  carsggect  31576  reprval  31881  repr0  31882  reprsuc  31886  reprss  31888  reprinrn  31889  reprlt  31890  reprgt  31892  reprinfz1  31893  reprpmtf1o  31897  reprdifc  31898  bnj1413  32307  cvmliftmolem1  32528  satf0suclem  32622  nosupno  33203  sssslt1  33260  sssslt2  33261  fwddifval  33623  neibastop1  33707  neibastop2lem  33708  fnejoin1  33716  filnetlem3  33728  filnetlem4  33729  bj-imdirval2  34472  bj-imdirval3  34473  dissneqlem  34620  selvval2lemn  39133  selvval2lem4  39134  selvval2lem5  39135  selvcl  39136  elrfi  39289  elrfirn2  39291  clcnvlem  39981  relexpss1d  40048  k0004lem2  40496  ixpssmapc  41334  restuni4  41385  wessf1ornlem  41443  unirnmap  41469  inmap  41470  difmapsn  41473  unirnmapsn  41475  ssmapsn  41477  limsupre  41920  limsuppnfdlem  41980  limsuppnflem  41989  limsupmnflem  41999  limsupre2lem  42003  liminfval4  42068  liminfval3  42069  icccncfext  42168  dvdivcncf  42210  dvnprodlem1  42229  dvnprodlem2  42230  ovolsplit  42272  stoweidlem31  42315  stoweidlem53  42337  stoweidlem57  42341  stoweidlem59  42343  etransclem46  42564  saliuncl  42606  salexct  42616  subsaluni  42642  fsumlesge0  42658  sge0f1o  42663  sge0iunmptlemfi  42694  sge0iunmptlemre  42696  meadjuni  42738  meadjiunlem  42746  omessle  42779  omecl  42784  isomenndlem  42811  caragencmpl  42816  ovnval2  42826  ovnval2b  42833  ovncvrrp  42845  ovncl  42848  hoidmvlelem2  42877  hoidmvlelem3  42878  ovncvr2  42892  ovnsubadd2lem  42926  ovnovollem3  42939  vonvolmbllem  42941  vonvolmbl  42942  sssmf  43014  incsmf  43018  issmflelem  43020  issmfle  43021  smfconst  43025  issmfgtlem  43031  issmfgt  43032  smfaddlem2  43039  decsmf  43042  issmfgelem  43044  issmfge  43045  nsssmfmbflem  43053  smfpimioo  43061  smfresal  43062  smfmullem4  43068  smfpimbor1lem1  43072  smf2id  43075  upwlksfval  44009