Theorem ssexd 5324

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3473   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  sselpwd  5326  opabbrex  7463  soex  7916  fex2  7928  funexw  7942  opabex2  8047  fnwelem  8122  fnse  8124  extmptsuppeq  8178  f1setex  8857  f1imaen2g  9017  ordtypelem10  9528  oismo  9541  wofib  9546  wdom2d  9581  wdomd  9582  unxpwdom2  9589  ttrclexg  9724  djuexALT  9923  acni2  10047  fin1a2lem12  10412  hsmexlem1  10427  zorn2lem4  10500  fpwwe2lem2  10633  fpwwe2lem4  10635  fpwwe2lem11  10642  fpwwe2  10644  fpwwelem  10646  canthwelem  10651  pwfseqlem4  10663  hashf1lem1  14422  trclfv  14954  hashbcss  16944  strssd  17146  restid2  17383  divsfval  17500  mrieqv2d  17590  mrissmrcd  17591  mreexexlemd  17595  mreexexlem3d  17597  mreexexlem4d  17598  mreexdomd  17600  rescabs  17789  rescabsOLD  17790  rescabs2  17791  resssetc  18052  resscatc  18069  estrres  18101  yonedalem1  18235  yonedalem21  18236  yonedalem3a  18237  yonedalem4c  18240  yonedalem22  18241  yonedalem3b  18242  yonedainv  18244  yonffthlem  18245  joinfval  18336  meetfval  18350  acsdomd  18520  gass  19213  permsetexOLD  19285  pmtrfconj  19382  sylow2blem2  19537  dprdres  19946  dmdprdsplitlem  19955  primefld  20652  pwssplit0  20902  pwssplit1  20903  pwssplit2  20904  pwssplit3  20905  frlmsplit2  21638  frlmsslss  21639  opsrtoslem2  21928  evlsgsumadd  21965  evlsgsummul  21966  evls1gsumadd  22163  evls1gsummul  22164  evl1gsummul  22199  neiptoptop  22955  lpval  22963  neitr  23004  ordtbaslem  23012  ordtrest2  23028  cnrest2  23110  cnpresti  23112  cnprest  23113  cnprest2  23114  connsuba  23244  connsubclo  23248  unconn  23253  1stcelcls  23285  hausmapdom  23324  dissnref  23352  ptbasfi  23405  ptcls  23440  cnmpt2res  23501  qtopval2  23520  elqtop  23521  qtoprest  23541  ptuncnv  23631  ptunhmeo  23632  fsubbas  23691  elfm  23771  rnelfmlem  23776  rnelfm  23777  fmfnfmlem4  23781  flimclslem  23808  hauspwpwdom  23812  ptcmplem1  23876  cnextcn  23891  cnextfres1  23892  isust  24028  trust  24054  elutop  24058  restutop  24062  trcfilu  24119  cfiluweak  24120  psmetres2  24140  xmetres2  24187  fmcfil  25120  dvaddf  25793  dvmulf  25794  dvcmulf  25796  dvcof  25800  ulmss  26248  nosupno  27549  noinfno  27564  sssslt1  27641  sssslt2  27642  sltonex  28067  perpln1  28394  perpln2  28395  isperp  28396  wksfval  29299  fnpreimac  32329  resf1o  32388  gsumpart  32643  cycpmco2lem5  32725  fldgenval  32838  islinds5  32920  ellspds  32921  elrsp  32926  elrspunidl  32986  resssra  33128  lbsdiflsp0  33165  irngval  33204  ordtrest2NEW  33367  lmlim  33391  esummono  33516  esumrnmpt2  33530  esumpinfval  33535  elcarsg  33768  carsgmon  33777  carsggect  33781  reprval  34086  repr0  34087  reprsuc  34091  reprss  34093  reprinrn  34094  reprlt  34095  reprgt  34097  reprinfz1  34098  reprpmtf1o  34102  reprdifc  34103  bnj1413  34510  cvmliftmolem1  34736  satf0suclem  34830  fwddifval  35604  neibastop1  35708  neibastop2lem  35709  fnejoin1  35717  filnetlem3  35729  filnetlem4  35730  bj-imdirval2lem  36527  bj-imdirval3  36529  bj-imdirco  36535  dissneqlem  36685  sticksstones20  41449  fsuppss  41532  psrbagres  41578  selvcllemh  41615  selvcllem4  41616  selvcllem5  41617  selvcl  41618  selvval2  41619  selvvvval  41620  evlselv  41622  selvadd  41623  selvmul  41624  fsuppssindlem2  41627  fsuppssind  41628  elrfi  41895  elrfirn2  41897  oaun3lem3  42589  nadd2rabex  42599  clcnvlem  42837  relexpss1d  42919  k0004lem2  43362  ixpssmapc  44223  restuni4  44272  restsubel  44309  wessf1ornlem  44343  disjinfi  44350  unirnmap  44366  inmap  44367  difmapsn  44370  unirnmapsn  44372  ssmapsn  44374  limsupre  44816  limsuppnfdlem  44876  limsuppnflem  44885  limsupmnflem  44895  limsupre2lem  44899  liminfval4  44964  liminfval3  44965  icccncfext  45062  dvdivcncf  45102  dvnprodlem1  45121  dvnprodlem2  45122  ovolsplit  45163  stoweidlem31  45206  stoweidlem53  45228  stoweidlem57  45232  stoweidlem59  45234  etransclem46  45455  salexct  45509  subsaluni  45535  fsumlesge0  45552  sge0f1o  45557  sge0iunmptlemfi  45588  sge0iunmptlemre  45590  meadjuni  45632  meadjiunlem  45640  omessle  45673  omecl  45678  isomenndlem  45705  caragencmpl  45710  ovnval2  45720  ovnval2b  45727  ovncvrrp  45739  ovncl  45742  hoidmvlelem2  45771  hoidmvlelem3  45772  ovncvr2  45786  ovnsubadd2lem  45820  ovnovollem3  45833  vonvolmbllem  45835  vonvolmbl  45836  sssmf  45913  incsmf  45917  issmflelem  45919  issmfle  45920  smfconst  45924  issmfgtlem  45930  issmfgt  45931  smfaddlem2  45939  decsmf  45942  issmfgelem  45944  issmfge  45945  nsssmfmbflem  45953  smfpimioo  45962  smfresal  45963  smfmullem4  45969  smfpimbor1lem1  45973  smf2id  45976  upwlksfval  46972  toplatglb  47788