Theorem ssexd 5293

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  abexd  5294  sselpwd  5297  sepab  5301  moabex  5437  opabbrex  7469  soex  7921  fex2  7936  fabexd  7937  mapex  7940  funexw  7952  opabex2  8057  fnwelem  8132  fnse  8134  extmptsuppeq  8189  f1setex  8861  f1imaen2g  9024  fsuppss  9356  ordtypelem10  9502  oismo  9515  wofib  9520  wdom2d  9555  wdomd  9556  unxpwdom2  9563  ttrclexg  9705  djuexALT  9930  acni2  10052  fin1a2lem12  10416  hsmexlem1  10431  zorn2lem4  10504  ondomon  10574  fpwwe2lem2  10644  fpwwe2lem4  10646  fpwwe2lem11  10653  fpwwe2  10655  fpwwelem  10657  canthwelem  10662  pwfseqlem4  10674  hashpss  14476  hashf1lem1  14522  trclfv  15075  hashbcss  17100  strssd  17301  restid2  17519  divsfval  17637  mrieqv2d  17731  mrissmrcd  17732  mreexexlemd  17736  mreexexlem3d  17738  mreexexlem4d  17739  mreexdomd  17741  rescabs  17926  rescabs2  17927  resssetc  18185  resscatc  18202  estrres  18231  yonedalem1  18364  yonedalem21  18365  yonedalem3a  18366  yonedalem4c  18369  yonedalem22  18370  yonedalem3b  18371  yonedainv  18373  yonffthlem  18374  joinfval  18463  meetfval  18477  acsdomd  18649  idressid  18779  ressmulgnnd  19202  gass  19429  pmtrfconj  19594  sylow2blem2  19749  dprdres  20158  dmdprdsplitlem  20167  primefld  20972  pwssplit0  21243  pwssplit1  21244  pwssplit2  21245  pwssplit3  21246  frlmsplit2  21987  frlmsslss  21988  psrbagres  22146  opsrtoslem2  22273  evlsgsumadd  22313  evlsgsummul  22314  selvcllemh  22354  selvcllem4  22355  selvcllem5  22356  selvcl  22357  selvval2  22358  selvvvval  22359  selvadd  22360  selvmul  22361  evls1gsumadd  22550  evls1gsummul  22551  evl1gsummul  22586  neiptoptop  23357  lpval  23365  neitr  23406  ordtbaslem  23414  ordtrest2  23430  cnrest2  23512  cnpresti  23514  cnprest  23515  cnprest2  23516  connsuba  23646  connsubclo  23650  unconn  23655  1stcelcls  23688  hausmapdom  23727  dissnref  23755  ptbasfi  23808  ptcls  23843  cnmpt2res  23904  qtopval2  23923  elqtop  23924  qtoprest  23944  ptuncnv  24034  ptunhmeo  24035  fsubbas  24094  elfm  24174  rnelfmlem  24179  rnelfm  24180  fmfnfmlem4  24184  flimclslem  24211  hauspwpwdom  24215  ptcmplem1  24279  cnextcn  24294  cnextfres1  24295  isust  24431  trust  24456  elutop  24460  restutop  24464  trcfilu  24520  cfiluweak  24521  psmetres2  24541  xmetres2  24588  fmcfil  25501  dvaddf  26171  dvmulf  26172  dvcmulf  26174  dvcof  26177  ulmss  26630  nosupno  27937  noinfno  27952  ssslts1  28036  ssslts2  28037  ltonsex  28525  perpln1  29062  perpln2  29063  isperp  29064  wksfval  30055  fnpreimac  33130  fisuppov1  33142  resf1o  33188  gsumpart  33490  gsumwrd2dccat  33505  cycpmco2lem5  33557  elrgspnlem1  33669  elrgspnlem2  33670  elrgspnlem3  33671  elrgspnlem4  33672  elrgspn  33673  erlval  33685  rlocval  33686  rlocbas  33695  fldgenval  33740  islinds5  33789  ellspds  33790  elrsp  33793  elrspunidl  33843  mplasclco  34013  selvascl  34014  evlextv  34039  psrmonprod  34049  esplympl  34064  resssra  34084  lbslelsp  34095  lbsdiflsp0  34123  irngval  34182  ordtrest2NEW  34420  lmlim  34444  esummono  34551  esumrnmpt2  34565  esumpinfval  34570  elcarsg  34803  carsgmon  34812  carsggect  34816  reprval  35105  repr0  35106  reprsuc  35110  reprss  35112  reprinrn  35113  reprlt  35114  reprgt  35116  reprinfz1  35117  reprpmtf1o  35121  reprdifc  35122  bnj1413  35531  cvmliftmolem1  35847  satf0suclem  35941  fwddifval  36729  neibastop1  36965  neibastop2lem  36966  fnejoin1  36974  filnetlem3  36986  filnetlem4  36987  weiunse  37074  numiunnum  37076  bj-imdirval2lem  37921  bj-imdirval3  37923  bj-imdirco  37929  dissneqlem  38081  aks6d1c2lem4  42980  sticksstones20  43019  aks6d1c6lem3  43025  evlselv  43422  fsuppssindlem2  43425  fsuppssind  43426  elrfi  43526  elrfirn2  43528  oaun3lem3  44204  nadd2rabex  44214  clcnvlem  44450  relexpss1d  44532  k0004lem2  44975  ixpssmapc  45894  restuni4  45940  restsubel  45972  wessf1ornlem  46004  unirnmap  46025  inmap  46026  difmapsn  46029  unirnmapsn  46031  ssmapsn  46033  limsupre  46456  limsuppnfdlem  46516  limsuppnflem  46525  limsupmnflem  46535  limsupre2lem  46539  liminfval4  46604  liminfval3  46605  icccncfext  46702  dvdivcncf  46742  dvnprodlem1  46761  dvnprodlem2  46762  ovolsplit  46803  stoweidlem31  46846  stoweidlem53  46868  stoweidlem57  46872  stoweidlem59  46874  etransclem46  47095  salexct  47149  subsaluni  47175  fsumlesge0  47192  sge0iunmptlemfi  47228  sge0iunmptlemre  47230  meadjuni  47272  meadjiunlem  47280  omessle  47313  omecl  47318  isomenndlem  47345  caragencmpl  47350  ovnval2  47360  ovnval2b  47367  ovncvrrp  47379  ovncl  47382  hoidmvlelem2  47411  hoidmvlelem3  47412  ovncvr2  47426  ovnsubadd2lem  47460  ovnovollem3  47473  vonvolmbllem  47475  vonvolmbl  47476  sssmf  47553  incsmf  47557  issmflelem  47559  issmfle  47560  smfconst  47564  issmfgtlem  47570  issmfgt  47571  smfaddlem2  47579  decsmf  47582  issmfgelem  47584  issmfge  47585  nsssmfmbflem  47593  smfpimioo  47602  smfresal  47603  smfmullem4  47609  smfpimbor1lem1  47613  smf2id  47616  tmachlem-agreeself  47751  tmachlem-agreeprod  47752  tmachlem-uassst  47758  tmachlem-extpcover  47760  tmachlem-agreefin  47763  upwlksfval  49038  toplatglb  49914