Theorem ssexd 5290

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  abexd  5291  sselpwd  5294  sepab  5298  moabex  5430  opabbrex  7493  soex  7954  fex2  7969  fabexd  7970  mapex  7973  funexw  7985  opabex2  8090  fnwelem  8167  fnse  8174  extmptsuppeq  8230  f1setex  8904  f1imaen2g  9067  fsuppss  9399  ordtypelem10  9545  oismo  9558  wofib  9563  wdom2d  9598  wdomd  9599  unxpwdom2  9606  ttrclexg  9748  djuexALT  10027  acni2  10149  fin1a2lem12  10513  hsmexlem1  10528  zorn2lem4  10601  ondomon  10671  fpwwe2lem2  10741  fpwwe2lem4  10743  fpwwe2lem11  10750  fpwwe2  10752  fpwwelem  10754  canthwelem  10759  pwfseqlem4  10771  hashpss  14578  hashf1lem1  14624  trclfv  15179  hashbcss  17208  strssd  17409  restid2  17627  divsfval  17745  mrieqv2d  17839  mrissmrcd  17840  mreexexlemd  17844  mreexexlem3d  17846  mreexexlem4d  17847  mreexdomd  17849  rescabs  18034  rescabs2  18035  resssetc  18293  resscatc  18310  estrres  18339  yonedalem1  18472  yonedalem21  18473  yonedalem3a  18474  yonedalem4c  18477  yonedalem22  18478  yonedalem3b  18479  yonedainv  18481  yonffthlem  18482  joinfval  18571  meetfval  18585  acsmapd  18754  acsdomd  18757  idressid  18888  ressmulgnnd  19314  gass  19542  pmtrfconj  19707  sylow2blem2  19862  dprdres  20271  dmdprdsplitlem  20280  primefld  21089  pwssplit0  21360  pwssplit1  21361  pwssplit2  21362  pwssplit3  21363  frlmsplit2  22106  frlmsslss  22107  psrbagres  22265  opsrtoslem2  22392  evlsgsumadd  22432  evlsgsummul  22433  selvcllemh  22473  selvcllem4  22474  selvcllem5  22475  selvcl  22476  selvval2  22477  selvvvval  22478  selvadd  22479  selvmul  22480  evls1gsumadd  22669  evls1gsummul  22670  evl1gsummul  22705  neiptoptop  23476  lpval  23484  neitr  23525  ordtbaslem  23533  ordtrest2  23549  cnrest2  23631  cnpresti  23633  cnprest  23634  cnprest2  23635  connsuba  23765  connsubclo  23769  unconn  23774  1stcelcls  23807  hausmapdom  23846  dissnref  23874  ptbasfi  23927  ptcls  23962  cnmpt2res  24023  qtopval2  24042  elqtop  24043  qtoprest  24063  ptuncnv  24153  ptunhmeo  24154  fsubbas  24213  elfm  24293  rnelfmlem  24298  rnelfm  24299  fmfnfmlem4  24303  flimclslem  24330  hauspwpwdom  24334  ptcmplem1  24398  cnextcn  24413  cnextfres1  24414  isust  24550  trust  24575  elutop  24579  restutop  24583  trcfilu  24639  cfiluweak  24640  psmetres2  24660  xmetres2  24707  fmcfil  25620  dvaddf  26289  dvmulf  26290  dvcmulf  26292  dvcof  26295  ulmss  26751  nosupno  28087  noinfno  28102  ssslts1  28186  ssslts2  28187  ltonsex  28675  perpln1  29212  perpln2  29213  isperp  29214  wksfval  30217  fnpreimac  33333  fisuppov1  33344  resf1o  33389  gsumpart  33691  gsumwrd2dccat  33706  cycpmco2lem5  33758  elrgspnlem1  33870  elrgspnlem2  33871  elrgspnlem3  33872  elrgspnlem4  33873  elrgspn  33874  erlval  33886  rlocval  33887  rlocbas  33896  fldgenval  33941  islinds5  33990  ellspds  33991  elrsp  33994  elrspunidl  34045  mplasclco  34215  selvascl  34216  evlextv  34241  psrmonprod  34251  esplympl  34266  resssra  34286  lbslelsp  34297  lbsdiflsp0  34325  irngval  34384  reff  34538  ordtrest2NEW  34622  lmlim  34646  esummono  34753  esumrnmpt2  34767  esumpinfval  34772  omssubadd  34999  elcarsg  35004  carsgmon  35013  carsggect  35017  reprval  35306  repr0  35307  reprsuc  35311  reprss  35313  reprinrn  35314  reprlt  35315  reprgt  35317  reprinfz1  35318  reprpmtf1o  35322  reprdifc  35323  bnj1413  35732  cvmliftmolem1  36212  satf0suclem  36306  fwddifval  37104  neibastop1  37324  neibastop2lem  37325  fnejoin1  37333  filnetlem3  37345  filnetlem4  37346  weiunse  37433  numiunnum  37435  bj-imdirval2lem  38294  bj-imdirval3  38296  bj-imdirco  38302  dissneqlem  38454  aks6d1c2lem4  43368  sticksstones20  43407  aks6d1c6lem3  43413  evlselv  43808  fsuppssindlem2  43811  fsuppssind  43812  elrfi  43896  elrfirn2  43898  oaun3lem3  44568  nadd2rabex  44578  clcnvlem  44813  relexpss1d  44895  k0004lem2  45338  mpoexwd  46116  ixpssmapc  46293  restuni4  46339  restsubel  46371  wessf1ornlem  46403  unirnmap  46424  inmap  46425  difmapsn  46428  unirnmapsn  46430  ssmapsn  46432  limsupre  46854  limsuppnfdlem  46914  limsuppnflem  46923  limsupmnflem  46933  limsupre2lem  46937  liminfval4  47002  liminfval3  47003  icccncfext  47100  dvdivcncf  47140  dvnprodlem1  47159  dvnprodlem2  47160  ovolsplit  47201  stoweidlem31  47244  stoweidlem53  47266  stoweidlem57  47270  stoweidlem59  47272  etransclem46  47493  salexct  47547  subsaluni  47573  fsumlesge0  47590  sge0iunmptlemfi  47626  sge0iunmptlemre  47628  meadjuni  47670  meadjiunlem  47678  omessle  47711  omecl  47716  isomenndlem  47743  caragencmpl  47748  ovnval2  47758  ovnval2b  47765  ovncvrrp  47777  ovncl  47780  hoidmvlelem2  47809  hoidmvlelem3  47810  ovncvr2  47824  ovnsubadd2lem  47858  ovnovollem3  47871  vonvolmbllem  47873  vonvolmbl  47874  sssmf  47951  incsmf  47955  issmflelem  47957  issmfle  47958  smfconst  47962  issmfgtlem  47968  issmfgt  47969  smfaddlem2  47977  decsmf  47980  issmfgelem  47982  issmfge  47983  nsssmfmbflem  47991  smfpimioo  48000  smfresal  48001  smfmullem4  48007  smfpimbor1lem1  48011  smf2id  48014  tmachlem-agreeself  48149  tmachlem-agreeprod  48150  tmachlem-uassst  48156  tmachlem-extpcover  48158  tmachlem-agreefin  48161  upwlksfval  49436  toplatglb  50318