Theorem ssexd 5282

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

Syntax hints:   → wi 4   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-sep 5248

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417  df-v 3458  df-in 3913  df-ss 3923

This theorem is referenced by:  abexd  5283  sselpwd  5286  moabex  5427  opabbrex  7451  soex  7904  fex2  7919  fabexd  7920  mapex  7923  funexw  7935  opabex2  8040  fnwelem  8113  fnse  8115  extmptsuppeq  8170  f1setex  8840  f1imaen2g  8998  fsuppss  9331  ordtypelem10  9477  oismo  9490  wofib  9495  wdom2d  9530  wdomd  9531  unxpwdom2  9538  ttrclexg  9680  djuexALT  9882  acni2  10004  fin1a2lem12  10370  hsmexlem1  10385  zorn2lem4  10458  ondomon  10522  fpwwe2lem2  10592  fpwwe2lem4  10594  fpwwe2lem11  10601  fpwwe2  10603  fpwwelem  10605  canthwelem  10610  pwfseqlem4  10622  hashf1lem1  14470  trclfv  15015  hashbcss  17042  strssd  17243  restid2  17461  divsfval  17579  mrieqv2d  17673  mrissmrcd  17674  mreexexlemd  17678  mreexexlem3d  17680  mreexexlem4d  17681  mreexdomd  17683  rescabs  17868  rescabs2  17869  resssetc  18127  resscatc  18144  estrres  18173  yonedalem1  18306  yonedalem21  18307  yonedalem3a  18308  yonedalem4c  18311  yonedalem22  18312  yonedalem3b  18313  yonedainv  18315  yonffthlem  18316  joinfval  18405  meetfval  18419  acsdomd  18591  ressmulgnnd  19122  gass  19343  pmtrfconj  19508  sylow2blem2  19663  dprdres  20072  dmdprdsplitlem  20081  primefld  20856  pwssplit0  21127  pwssplit1  21128  pwssplit2  21129  pwssplit3  21130  frlmsplit2  21827  frlmsslss  21828  psrbagres  21984  opsrtoslem2  22111  evlsgsumadd  22151  evlsgsummul  22152  selvcllemh  22192  selvcllem4  22193  selvcllem5  22194  selvcl  22195  selvval2  22196  selvvvval  22197  selvadd  22198  selvmul  22199  evls1gsumadd  22389  evls1gsummul  22390  evl1gsummul  22425  neiptoptop  23193  lpval  23201  neitr  23242  ordtbaslem  23250  ordtrest2  23266  cnrest2  23348  cnpresti  23350  cnprest  23351  cnprest2  23352  connsuba  23482  connsubclo  23486  unconn  23491  1stcelcls  23523  hausmapdom  23562  dissnref  23590  ptbasfi  23643  ptcls  23678  cnmpt2res  23739  qtopval2  23758  elqtop  23759  qtoprest  23779  ptuncnv  23869  ptunhmeo  23870  fsubbas  23929  elfm  24009  rnelfmlem  24014  rnelfm  24015  fmfnfmlem4  24019  flimclslem  24046  hauspwpwdom  24050  ptcmplem1  24114  cnextcn  24129  cnextfres1  24130  isust  24266  trust  24291  elutop  24295  restutop  24299  trcfilu  24355  cfiluweak  24356  psmetres2  24376  xmetres2  24423  fmcfil  25336  dvaddf  26006  dvmulf  26007  dvcmulf  26009  dvcof  26012  ulmss  26462  nosupno  27769  noinfno  27784  ssslts1  27868  ssslts2  27869  ltonsex  28357  perpln1  28885  perpln2  28886  isperp  28887  wksfval  29812  fnpreimac  32874  fisuppov1  32887  resf1o  32934  hashpss  33013  gsumpart  33245  gsumwrd2dccat  33260  cycpmco2lem5  33312  elrgspnlem1  33425  elrgspnlem2  33426  elrgspnlem3  33427  elrgspnlem4  33428  elrgspn  33429  erlval  33441  rlocval  33442  rlocbas  33451  fldgenval  33501  islinds5  33555  ellspds  33556  elrsp  33560  elrspunidl  33616  mplasclco  33815  selvascl  33816  evlextv  33841  psrmonprod  33851  esplympl  33866  resssra  33886  lbslelsp  33897  lbsdiflsp0  33925  irngval  33984  ordtrest2NEW  34222  lmlim  34246  esummono  34353  esumrnmpt2  34367  esumpinfval  34372  elcarsg  34604  carsgmon  34613  carsggect  34617  reprval  34906  repr0  34907  reprsuc  34911  reprss  34913  reprinrn  34914  reprlt  34915  reprgt  34917  reprinfz1  34918  reprpmtf1o  34922  reprdifc  34923  bnj1413  35332  cvmliftmolem1  35636  satf0suclem  35730  fwddifval  36517  neibastop1  36724  neibastop2lem  36725  fnejoin1  36733  filnetlem3  36745  filnetlem4  36746  weiunse  36833  numiunnum  36835  bj-imdirval2lem  37679  bj-imdirval3  37681  bj-imdirco  37687  dissneqlem  37839  aks6d1c2lem4  42749  sticksstones20  42788  aks6d1c6lem3  42794  evlselv  43176  fsuppssindlem2  43179  fsuppssind  43180  elrfi  43280  elrfirn2  43282  oaun3lem3  43958  nadd2rabex  43968  clcnvlem  44204  relexpss1d  44286  k0004lem2  44729  ixpssmapc  45658  restuni4  45704  restsubel  45736  wessf1ornlem  45768  disjinfi  45775  unirnmap  45789  inmap  45790  difmapsn  45793  unirnmapsn  45795  ssmapsn  45797  limsupre  46220  limsuppnfdlem  46280  limsuppnflem  46289  limsupmnflem  46299  limsupre2lem  46303  liminfval4  46368  liminfval3  46369  icccncfext  46466  dvdivcncf  46506  dvnprodlem1  46525  dvnprodlem2  46526  ovolsplit  46567  stoweidlem31  46610  stoweidlem53  46632  stoweidlem57  46636  stoweidlem59  46638  etransclem46  46859  salexct  46913  subsaluni  46939  fsumlesge0  46956  sge0iunmptlemfi  46992  sge0iunmptlemre  46994  meadjuni  47036  meadjiunlem  47044  omessle  47077  omecl  47082  isomenndlem  47109  caragencmpl  47114  ovnval2  47124  ovnval2b  47131  ovncvrrp  47143  ovncl  47146  hoidmvlelem2  47175  hoidmvlelem3  47176  ovncvr2  47190  ovnsubadd2lem  47224  ovnovollem3  47237  vonvolmbllem  47239  vonvolmbl  47240  sssmf  47317  incsmf  47321  issmflelem  47323  issmfle  47324  smfconst  47328  issmfgtlem  47334  issmfgt  47335  smfaddlem2  47343  decsmf  47346  issmfgelem  47348  issmfge  47349  nsssmfmbflem  47357  smfpimioo  47366  smfresal  47367  smfmullem4  47373  smfpimbor1lem1  47377  smf2id  47380  upwlksfval  48762  toplatglb  49627