Theorem ssexd 5294

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-in 3911  df-ss 3921

This theorem is used by:  abexd  5295  sselpwd  5298  sepab  5302  moabex  5438  opabbrex  7465  soex  7916  fex2  7931  fabexd  7932  mapex  7935  funexw  7947  opabex2  8052  fnwelem  8125  fnse  8127  extmptsuppeq  8182  f1setex  8852  f1imaen2g  9010  fsuppss  9341  ordtypelem10  9487  oismo  9500  wofib  9505  wdom2d  9540  wdomd  9541  unxpwdom2  9548  ttrclexg  9690  djuexALT  9915  acni2  10037  fin1a2lem12  10401  hsmexlem1  10416  zorn2lem4  10489  ondomon  10553  fpwwe2lem2  10623  fpwwe2lem4  10625  fpwwe2lem11  10632  fpwwe2  10634  fpwwelem  10636  canthwelem  10641  pwfseqlem4  10653  hashpss  14453  hashf1lem1  14499  trclfv  15044  hashbcss  17070  strssd  17271  restid2  17489  divsfval  17607  mrieqv2d  17701  mrissmrcd  17702  mreexexlemd  17706  mreexexlem3d  17708  mreexexlem4d  17709  mreexdomd  17711  rescabs  17896  rescabs2  17897  resssetc  18155  resscatc  18172  estrres  18201  yonedalem1  18334  yonedalem21  18335  yonedalem3a  18336  yonedalem4c  18339  yonedalem22  18340  yonedalem3b  18341  yonedainv  18343  yonffthlem  18344  joinfval  18433  meetfval  18447  acsdomd  18619  ressmulgnnd  19150  gass  19377  pmtrfconj  19542  sylow2blem2  19697  dprdres  20106  dmdprdsplitlem  20115  primefld  20919  pwssplit0  21190  pwssplit1  21191  pwssplit2  21192  pwssplit3  21193  frlmsplit2  21934  frlmsslss  21935  psrbagres  22091  opsrtoslem2  22218  evlsgsumadd  22258  evlsgsummul  22259  selvcllemh  22299  selvcllem4  22300  selvcllem5  22301  selvcl  22302  selvval2  22303  selvvvval  22304  selvadd  22305  selvmul  22306  evls1gsumadd  22495  evls1gsummul  22496  evl1gsummul  22531  neiptoptop  23299  lpval  23307  neitr  23348  ordtbaslem  23356  ordtrest2  23372  cnrest2  23454  cnpresti  23456  cnprest  23457  cnprest2  23458  connsuba  23588  connsubclo  23592  unconn  23597  1stcelcls  23629  hausmapdom  23668  dissnref  23696  ptbasfi  23749  ptcls  23784  cnmpt2res  23845  qtopval2  23864  elqtop  23865  qtoprest  23885  ptuncnv  23975  ptunhmeo  23976  fsubbas  24035  elfm  24115  rnelfmlem  24120  rnelfm  24121  fmfnfmlem4  24125  flimclslem  24152  hauspwpwdom  24156  ptcmplem1  24220  cnextcn  24235  cnextfres1  24236  isust  24372  trust  24397  elutop  24401  restutop  24405  trcfilu  24461  cfiluweak  24462  psmetres2  24482  xmetres2  24529  fmcfil  25442  dvaddf  26112  dvmulf  26113  dvcmulf  26115  dvcof  26118  ulmss  26571  nosupno  27878  noinfno  27893  ssslts1  27977  ssslts2  27978  ltonsex  28466  perpln1  29001  perpln2  29002  isperp  29003  wksfval  29970  fnpreimac  33026  fisuppov1  33039  resf1o  33086  gsumpart  33392  gsumwrd2dccat  33407  cycpmco2lem5  33459  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnlem3  33573  elrgspnlem4  33574  elrgspn  33575  erlval  33587  rlocval  33588  rlocbas  33597  fldgenval  33642  islinds5  33691  ellspds  33692  elrsp  33695  elrspunidl  33745  mplasclco  33915  selvascl  33916  evlextv  33941  psrmonprod  33951  esplympl  33966  resssra  33986  lbslelsp  33997  lbsdiflsp0  34025  irngval  34084  ordtrest2NEW  34322  lmlim  34346  esummono  34453  esumrnmpt2  34467  esumpinfval  34472  elcarsg  34704  carsgmon  34713  carsggect  34717  reprval  35006  repr0  35007  reprsuc  35011  reprss  35013  reprinrn  35014  reprlt  35015  reprgt  35017  reprinfz1  35018  reprpmtf1o  35022  reprdifc  35023  bnj1413  35432  cvmliftmolem1  35781  satf0suclem  35875  fwddifval  36662  neibastop1  36898  neibastop2lem  36899  fnejoin1  36907  filnetlem3  36919  filnetlem4  36920  weiunse  37007  numiunnum  37009  bj-imdirval2lem  37854  bj-imdirval3  37856  bj-imdirco  37862  dissneqlem  38014  aks6d1c2lem4  42922  sticksstones20  42961  aks6d1c6lem3  42967  evlselv  43349  fsuppssindlem2  43352  fsuppssind  43353  elrfi  43453  elrfirn2  43455  oaun3lem3  44131  nadd2rabex  44141  clcnvlem  44377  relexpss1d  44459  k0004lem2  44902  ixpssmapc  45821  restuni4  45867  restsubel  45899  wessf1ornlem  45931  disjinfi  45938  unirnmap  45952  inmap  45953  difmapsn  45956  unirnmapsn  45958  ssmapsn  45960  limsupre  46383  limsuppnfdlem  46443  limsuppnflem  46452  limsupmnflem  46462  limsupre2lem  46466  liminfval4  46531  liminfval3  46532  icccncfext  46629  dvdivcncf  46669  dvnprodlem1  46688  dvnprodlem2  46689  ovolsplit  46730  stoweidlem31  46773  stoweidlem53  46795  stoweidlem57  46799  stoweidlem59  46801  etransclem46  47022  salexct  47076  subsaluni  47102  fsumlesge0  47119  sge0iunmptlemfi  47155  sge0iunmptlemre  47157  meadjuni  47199  meadjiunlem  47207  omessle  47240  omecl  47245  isomenndlem  47272  caragencmpl  47277  ovnval2  47287  ovnval2b  47294  ovncvrrp  47306  ovncl  47309  hoidmvlelem2  47338  hoidmvlelem3  47339  ovncvr2  47353  ovnsubadd2lem  47387  ovnovollem3  47400  vonvolmbllem  47402  vonvolmbl  47403  sssmf  47480  incsmf  47484  issmflelem  47486  issmfle  47487  smfconst  47491  issmfgtlem  47497  issmfgt  47498  smfaddlem2  47506  decsmf  47509  issmfgelem  47511  issmfge  47512  nsssmfmbflem  47520  smfpimioo  47529  smfresal  47530  smfmullem4  47536  smfpimbor1lem1  47540  smf2id  47543  upwlksfval  48928  toplatglb  49807