Theorem ssexd 5342

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  abexd  5343  sselpwd  5346  opabbrex  7501  soex  7961  fex2  7974  fabexd  7975  mapex  7979  funexw  7992  opabex2  8098  fnwelem  8172  fnse  8174  extmptsuppeq  8229  f1setex  8915  f1imaen2g  9075  fsuppss  9452  ordtypelem10  9596  oismo  9609  wofib  9614  wdom2d  9649  wdomd  9650  unxpwdom2  9657  ttrclexg  9792  djuexALT  9991  acni2  10115  fin1a2lem12  10480  hsmexlem1  10495  zorn2lem4  10568  fpwwe2lem2  10701  fpwwe2lem4  10703  fpwwe2lem11  10710  fpwwe2  10712  fpwwelem  10714  canthwelem  10719  pwfseqlem4  10731  hashf1lem1  14504  trclfv  15049  hashbcss  17051  strssd  17253  restid2  17490  divsfval  17607  mrieqv2d  17697  mrissmrcd  17698  mreexexlemd  17702  mreexexlem3d  17704  mreexexlem4d  17705  mreexdomd  17707  rescabs  17896  rescabsOLD  17897  rescabs2  17898  resssetc  18159  resscatc  18176  estrres  18208  yonedalem1  18342  yonedalem21  18343  yonedalem3a  18344  yonedalem4c  18347  yonedalem22  18348  yonedalem3b  18349  yonedainv  18351  yonffthlem  18352  joinfval  18443  meetfval  18457  acsdomd  18627  ressmulgnnd  19118  gass  19341  pmtrfconj  19508  sylow2blem2  19663  dprdres  20072  dmdprdsplitlem  20081  primefld  20828  pwssplit0  21080  pwssplit1  21081  pwssplit2  21082  pwssplit3  21083  frlmsplit2  21816  frlmsslss  21817  opsrtoslem2  22103  evlsgsumadd  22138  evlsgsummul  22139  evls1gsumadd  22349  evls1gsummul  22350  evl1gsummul  22385  neiptoptop  23160  lpval  23168  neitr  23209  ordtbaslem  23217  ordtrest2  23233  cnrest2  23315  cnpresti  23317  cnprest  23318  cnprest2  23319  connsuba  23449  connsubclo  23453  unconn  23458  1stcelcls  23490  hausmapdom  23529  dissnref  23557  ptbasfi  23610  ptcls  23645  cnmpt2res  23706  qtopval2  23725  elqtop  23726  qtoprest  23746  ptuncnv  23836  ptunhmeo  23837  fsubbas  23896  elfm  23976  rnelfmlem  23981  rnelfm  23982  fmfnfmlem4  23986  flimclslem  24013  hauspwpwdom  24017  ptcmplem1  24081  cnextcn  24096  cnextfres1  24097  isust  24233  trust  24259  elutop  24263  restutop  24267  trcfilu  24324  cfiluweak  24325  psmetres2  24345  xmetres2  24392  fmcfil  25325  dvaddf  25999  dvmulf  26000  dvcmulf  26002  dvcof  26006  ulmss  26458  nosupno  27766  noinfno  27781  sssslt1  27858  sssslt2  27859  sltonex  28302  perpln1  28736  perpln2  28737  isperp  28738  wksfval  29645  fnpreimac  32689  resf1o  32744  gsumpart  33038  cycpmco2lem5  33123  erlval  33230  rlocval  33231  rlocbas  33239  fldgenval  33279  islinds5  33360  ellspds  33361  elrsp  33365  elrspunidl  33421  resssra  33602  lbsdiflsp0  33639  irngval  33685  ordtrest2NEW  33869  lmlim  33893  esummono  34018  esumrnmpt2  34032  esumpinfval  34037  elcarsg  34270  carsgmon  34279  carsggect  34283  reprval  34587  repr0  34588  reprsuc  34592  reprss  34594  reprinrn  34595  reprlt  34596  reprgt  34598  reprinfz1  34599  reprpmtf1o  34603  reprdifc  34604  bnj1413  35011  cvmliftmolem1  35249  satf0suclem  35343  fwddifval  36126  neibastop1  36325  neibastop2lem  36326  fnejoin1  36334  filnetlem3  36346  filnetlem4  36347  weiunse  36434  numiunnum  36436  bj-imdirval2lem  37148  bj-imdirval3  37150  bj-imdirco  37156  dissneqlem  37306  aks6d1c2lem4  42084  sticksstones20  42123  aks6d1c6lem3  42129  psrbagres  42501  selvcllemh  42535  selvcllem4  42536  selvcllem5  42537  selvcl  42538  selvval2  42539  selvvvval  42540  evlselv  42542  selvadd  42543  selvmul  42544  fsuppssindlem2  42547  fsuppssind  42548  elrfi  42650  elrfirn2  42652  oaun3lem3  43338  nadd2rabex  43348  clcnvlem  43585  relexpss1d  43667  k0004lem2  44110  ixpssmapc  44975  restuni4  45023  restsubel  45058  wessf1ornlem  45092  disjinfi  45099  unirnmap  45115  inmap  45116  difmapsn  45119  unirnmapsn  45121  ssmapsn  45123  limsupre  45562  limsuppnfdlem  45622  limsuppnflem  45631  limsupmnflem  45641  limsupre2lem  45645  liminfval4  45710  liminfval3  45711  icccncfext  45808  dvdivcncf  45848  dvnprodlem1  45867  dvnprodlem2  45868  ovolsplit  45909  stoweidlem31  45952  stoweidlem53  45974  stoweidlem57  45978  stoweidlem59  45980  etransclem46  46201  salexct  46255  subsaluni  46281  fsumlesge0  46298  sge0f1o  46303  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  meadjuni  46378  meadjiunlem  46386  omessle  46419  omecl  46424  isomenndlem  46451  caragencmpl  46456  ovnval2  46466  ovnval2b  46473  ovncvrrp  46485  ovncl  46488  hoidmvlelem2  46517  hoidmvlelem3  46518  ovncvr2  46532  ovnsubadd2lem  46566  ovnovollem3  46579  vonvolmbllem  46581  vonvolmbl  46582  sssmf  46659  incsmf  46663  issmflelem  46665  issmfle  46666  smfconst  46670  issmfgtlem  46676  issmfgt  46677  smfaddlem2  46685  decsmf  46688  issmfgelem  46690  issmfge  46691  nsssmfmbflem  46699  smfpimioo  46708  smfresal  46709  smfmullem4  46715  smfpimbor1lem1  46719  smf2id  46722  upwlksfval  47858  toplatglb  48673