Theorem ssexd 5285

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

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

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 2732  ax-sep 5248

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-in 3905  df-ss 3915

This theorem is used by:  abexd  5286  sselpwd  5289  sepab  5293  moabex  5425  opabbrex  7461  soex  7916  fex2  7931  fabexd  7932  mapex  7935  funexw  7947  opabex2  8051  fnwelem  8126  fnse  8128  extmptsuppeq  8183  f1setex  8857  f1imaen2g  9020  fsuppss  9353  ordtypelem10  9499  oismo  9512  wofib  9517  wdom2d  9552  wdomd  9553  unxpwdom2  9560  ttrclexg  9702  djuexALT  9974  acni2  10096  fin1a2lem12  10460  hsmexlem1  10475  zorn2lem4  10548  ondomon  10618  fpwwe2lem2  10688  fpwwe2lem4  10690  fpwwe2lem11  10697  fpwwe2  10699  fpwwelem  10701  canthwelem  10706  pwfseqlem4  10718  hashpss  14521  hashf1lem1  14567  trclfv  15120  hashbcss  17143  strssd  17344  restid2  17562  divsfval  17680  mrieqv2d  17774  mrissmrcd  17775  mreexexlemd  17779  mreexexlem3d  17781  mreexexlem4d  17782  mreexdomd  17784  rescabs  17969  rescabs2  17970  resssetc  18228  resscatc  18245  estrres  18274  yonedalem1  18407  yonedalem21  18408  yonedalem3a  18409  yonedalem4c  18412  yonedalem22  18413  yonedalem3b  18414  yonedainv  18416  yonffthlem  18417  joinfval  18506  meetfval  18520  acsdomd  18692  idressid  18823  ressmulgnnd  19249  gass  19476  pmtrfconj  19641  sylow2blem2  19796  dprdres  20205  dmdprdsplitlem  20214  primefld  21023  pwssplit0  21294  pwssplit1  21295  pwssplit2  21296  pwssplit3  21297  frlmsplit2  22040  frlmsslss  22041  psrbagres  22199  opsrtoslem2  22326  evlsgsumadd  22366  evlsgsummul  22367  selvcllemh  22407  selvcllem4  22408  selvcllem5  22409  selvcl  22410  selvval2  22411  selvvvval  22412  selvadd  22413  selvmul  22414  evls1gsumadd  22603  evls1gsummul  22604  evl1gsummul  22639  neiptoptop  23410  lpval  23418  neitr  23459  ordtbaslem  23467  ordtrest2  23483  cnrest2  23565  cnpresti  23567  cnprest  23568  cnprest2  23569  connsuba  23699  connsubclo  23703  unconn  23708  1stcelcls  23741  hausmapdom  23780  dissnref  23808  ptbasfi  23861  ptcls  23896  cnmpt2res  23957  qtopval2  23976  elqtop  23977  qtoprest  23997  ptuncnv  24087  ptunhmeo  24088  fsubbas  24147  elfm  24227  rnelfmlem  24232  rnelfm  24233  fmfnfmlem4  24237  flimclslem  24264  hauspwpwdom  24268  ptcmplem1  24332  cnextcn  24347  cnextfres1  24348  isust  24484  trust  24509  elutop  24513  restutop  24517  trcfilu  24573  cfiluweak  24574  psmetres2  24594  xmetres2  24641  fmcfil  25554  dvaddf  26223  dvmulf  26224  dvcmulf  26226  dvcof  26229  ulmss  26687  nosupno  27993  noinfno  28008  ssslts1  28092  ssslts2  28093  ltonsex  28581  perpln1  29118  perpln2  29119  isperp  29120  wksfval  30123  fnpreimac  33197  fisuppov1  33209  resf1o  33255  gsumpart  33557  gsumwrd2dccat  33572  cycpmco2lem5  33624  elrgspnlem1  33736  elrgspnlem2  33737  elrgspnlem3  33738  elrgspnlem4  33739  elrgspn  33740  erlval  33752  rlocval  33753  rlocbas  33762  fldgenval  33807  islinds5  33856  ellspds  33857  elrsp  33860  elrspunidl  33911  mplasclco  34081  selvascl  34082  evlextv  34107  psrmonprod  34117  esplympl  34132  resssra  34152  lbslelsp  34163  lbsdiflsp0  34191  irngval  34250  ordtrest2NEW  34488  lmlim  34512  esummono  34619  esumrnmpt2  34633  esumpinfval  34638  elcarsg  34871  carsgmon  34880  carsggect  34884  reprval  35173  repr0  35174  reprsuc  35178  reprss  35180  reprinrn  35181  reprlt  35182  reprgt  35184  reprinfz1  35185  reprpmtf1o  35189  reprdifc  35190  bnj1413  35599  cvmliftmolem1  35967  satf0suclem  36061  fwddifval  36849  neibastop1  37069  neibastop2lem  37070  fnejoin1  37078  filnetlem3  37090  filnetlem4  37091  weiunse  37178  numiunnum  37180  bj-imdirval2lem  38023  bj-imdirval3  38025  bj-imdirco  38031  dissneqlem  38183  aks6d1c2lem4  43097  sticksstones20  43136  aks6d1c6lem3  43142  evlselv  43539  fsuppssindlem2  43542  fsuppssind  43543  elrfi  43643  elrfirn2  43645  oaun3lem3  44321  nadd2rabex  44331  clcnvlem  44567  relexpss1d  44649  k0004lem2  45092  ixpssmapc  46011  restuni4  46057  restsubel  46089  wessf1ornlem  46121  unirnmap  46142  inmap  46143  difmapsn  46146  unirnmapsn  46148  ssmapsn  46150  limsupre  46573  limsuppnfdlem  46633  limsuppnflem  46642  limsupmnflem  46652  limsupre2lem  46656  liminfval4  46721  liminfval3  46722  icccncfext  46819  dvdivcncf  46859  dvnprodlem1  46878  dvnprodlem2  46879  ovolsplit  46920  stoweidlem31  46963  stoweidlem53  46985  stoweidlem57  46989  stoweidlem59  46991  etransclem46  47212  salexct  47266  subsaluni  47292  fsumlesge0  47309  sge0iunmptlemfi  47345  sge0iunmptlemre  47347  meadjuni  47389  meadjiunlem  47397  omessle  47430  omecl  47435  isomenndlem  47462  caragencmpl  47467  ovnval2  47477  ovnval2b  47484  ovncvrrp  47496  ovncl  47499  hoidmvlelem2  47528  hoidmvlelem3  47529  ovncvr2  47543  ovnsubadd2lem  47577  ovnovollem3  47590  vonvolmbllem  47592  vonvolmbl  47593  sssmf  47670  incsmf  47674  issmflelem  47676  issmfle  47677  smfconst  47681  issmfgtlem  47687  issmfgt  47688  smfaddlem2  47696  decsmf  47699  issmfgelem  47701  issmfge  47702  nsssmfmbflem  47710  smfpimioo  47719  smfresal  47720  smfmullem4  47726  smfpimbor1lem1  47730  smf2id  47733  tmachlem-agreeself  47868  tmachlem-agreeprod  47869  tmachlem-uassst  47875  tmachlem-extpcover  47877  tmachlem-agreefin  47880  upwlksfval  49155  toplatglb  50031