Theorem ssexd 5279

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  abexd  5280  sselpwd  5283  opabbrex  7440  soex  7897  fex2  7912  fabexd  7913  mapex  7917  funexw  7930  opabex2  8036  fnwelem  8110  fnse  8112  extmptsuppeq  8167  f1setex  8830  f1imaen2g  8986  fsuppss  9334  ordtypelem10  9480  oismo  9493  wofib  9498  wdom2d  9533  wdomd  9534  unxpwdom2  9541  ttrclexg  9676  djuexALT  9875  acni2  9999  fin1a2lem12  10364  hsmexlem1  10379  zorn2lem4  10452  fpwwe2lem2  10585  fpwwe2lem4  10587  fpwwe2lem11  10594  fpwwe2  10596  fpwwelem  10598  canthwelem  10603  pwfseqlem4  10615  hashf1lem1  14420  trclfv  14966  hashbcss  16975  strssd  17175  restid2  17393  divsfval  17510  mrieqv2d  17600  mrissmrcd  17601  mreexexlemd  17605  mreexexlem3d  17607  mreexexlem4d  17608  mreexdomd  17610  rescabs  17795  rescabs2  17796  resssetc  18054  resscatc  18071  estrres  18100  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedainv  18242  yonffthlem  18243  joinfval  18332  meetfval  18346  acsdomd  18516  ressmulgnnd  19010  gass  19233  pmtrfconj  19396  sylow2blem2  19551  dprdres  19960  dmdprdsplitlem  19969  primefld  20714  pwssplit0  20965  pwssplit1  20966  pwssplit2  20967  pwssplit3  20968  frlmsplit2  21682  frlmsslss  21683  opsrtoslem2  21963  evlsgsumadd  21998  evlsgsummul  21999  evls1gsumadd  22211  evls1gsummul  22212  evl1gsummul  22247  neiptoptop  23018  lpval  23026  neitr  23067  ordtbaslem  23075  ordtrest2  23091  cnrest2  23173  cnpresti  23175  cnprest  23176  cnprest2  23177  connsuba  23307  connsubclo  23311  unconn  23316  1stcelcls  23348  hausmapdom  23387  dissnref  23415  ptbasfi  23468  ptcls  23503  cnmpt2res  23564  qtopval2  23583  elqtop  23584  qtoprest  23604  ptuncnv  23694  ptunhmeo  23695  fsubbas  23754  elfm  23834  rnelfmlem  23839  rnelfm  23840  fmfnfmlem4  23844  flimclslem  23871  hauspwpwdom  23875  ptcmplem1  23939  cnextcn  23954  cnextfres1  23955  isust  24091  trust  24117  elutop  24121  restutop  24125  trcfilu  24181  cfiluweak  24182  psmetres2  24202  xmetres2  24249  fmcfil  25172  dvaddf  25845  dvmulf  25846  dvcmulf  25848  dvcof  25852  ulmss  26306  nosupno  27615  noinfno  27630  sssslt1  27707  sssslt2  27708  sltonex  28163  perpln1  28637  perpln2  28638  isperp  28639  wksfval  29537  fnpreimac  32595  fisuppov1  32606  resf1o  32653  hashpss  32734  gsumpart  32997  gsumwrd2dccat  33007  cycpmco2lem5  33087  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem3  33195  elrgspnlem4  33196  elrgspn  33197  erlval  33209  rlocval  33210  rlocbas  33218  fldgenval  33262  islinds5  33338  ellspds  33339  elrsp  33343  elrspunidl  33399  resssra  33583  lbslelsp  33593  lbsdiflsp0  33622  irngval  33680  ordtrest2NEW  33913  lmlim  33937  esummono  34044  esumrnmpt2  34058  esumpinfval  34063  elcarsg  34296  carsgmon  34305  carsggect  34309  reprval  34601  repr0  34602  reprsuc  34606  reprss  34608  reprinrn  34609  reprlt  34610  reprgt  34612  reprinfz1  34613  reprpmtf1o  34617  reprdifc  34618  bnj1413  35025  cvmliftmolem1  35268  satf0suclem  35362  fwddifval  36150  neibastop1  36347  neibastop2lem  36348  fnejoin1  36356  filnetlem3  36368  filnetlem4  36369  weiunse  36456  numiunnum  36458  bj-imdirval2lem  37170  bj-imdirval3  37172  bj-imdirco  37178  dissneqlem  37328  aks6d1c2lem4  42115  sticksstones20  42154  aks6d1c6lem3  42160  psrbagres  42534  selvcllemh  42568  selvcllem4  42569  selvcllem5  42570  selvcl  42571  selvval2  42572  selvvvval  42573  evlselv  42575  selvadd  42576  selvmul  42577  fsuppssindlem2  42580  fsuppssind  42581  elrfi  42682  elrfirn2  42684  oaun3lem3  43365  nadd2rabex  43375  clcnvlem  43612  relexpss1d  43694  k0004lem2  44137  ixpssmapc  45067  restuni4  45115  restsubel  45147  wessf1ornlem  45179  disjinfi  45186  unirnmap  45202  inmap  45203  difmapsn  45206  unirnmapsn  45208  ssmapsn  45210  limsupre  45639  limsuppnfdlem  45699  limsuppnflem  45708  limsupmnflem  45718  limsupre2lem  45722  liminfval4  45787  liminfval3  45788  icccncfext  45885  dvdivcncf  45925  dvnprodlem1  45944  dvnprodlem2  45945  ovolsplit  45986  stoweidlem31  46029  stoweidlem53  46051  stoweidlem57  46055  stoweidlem59  46057  etransclem46  46278  salexct  46332  subsaluni  46358  fsumlesge0  46375  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  meadjuni  46455  meadjiunlem  46463  omessle  46496  omecl  46501  isomenndlem  46528  caragencmpl  46533  ovnval2  46543  ovnval2b  46550  ovncvrrp  46562  ovncl  46565  hoidmvlelem2  46594  hoidmvlelem3  46595  ovncvr2  46609  ovnsubadd2lem  46643  ovnovollem3  46656  vonvolmbllem  46658  vonvolmbl  46659  sssmf  46736  incsmf  46740  issmflelem  46742  issmfle  46743  smfconst  46747  issmfgtlem  46753  issmfgt  46754  smfaddlem2  46762  decsmf  46765  issmfgelem  46767  issmfge  46768  nsssmfmbflem  46776  smfpimioo  46785  smfresal  46786  smfmullem4  46792  smfpimbor1lem1  46796  smf2id  46799  upwlksfval  48123  toplatglb  48989