Theorem ssexd 5294

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  abexd  5295  sselpwd  5298  opabbrex  7456  soex  7915  fex2  7930  fabexd  7931  mapex  7935  funexw  7948  opabex2  8054  fnwelem  8128  fnse  8130  extmptsuppeq  8185  f1setex  8869  f1imaen2g  9027  fsuppss  9393  ordtypelem10  9539  oismo  9552  wofib  9557  wdom2d  9592  wdomd  9593  unxpwdom2  9600  ttrclexg  9735  djuexALT  9934  acni2  10058  fin1a2lem12  10423  hsmexlem1  10438  zorn2lem4  10511  fpwwe2lem2  10644  fpwwe2lem4  10646  fpwwe2lem11  10653  fpwwe2  10655  fpwwelem  10657  canthwelem  10662  pwfseqlem4  10674  hashf1lem1  14471  trclfv  15017  hashbcss  17022  strssd  17222  restid2  17442  divsfval  17559  mrieqv2d  17649  mrissmrcd  17650  mreexexlemd  17654  mreexexlem3d  17656  mreexexlem4d  17657  mreexdomd  17659  rescabs  17844  rescabs2  17845  resssetc  18103  resscatc  18120  estrres  18149  yonedalem1  18282  yonedalem21  18283  yonedalem3a  18284  yonedalem4c  18287  yonedalem22  18288  yonedalem3b  18289  yonedainv  18291  yonffthlem  18292  joinfval  18381  meetfval  18395  acsdomd  18565  ressmulgnnd  19059  gass  19282  pmtrfconj  19445  sylow2blem2  19600  dprdres  20009  dmdprdsplitlem  20018  primefld  20763  pwssplit0  21014  pwssplit1  21015  pwssplit2  21016  pwssplit3  21017  frlmsplit2  21731  frlmsslss  21732  opsrtoslem2  22012  evlsgsumadd  22047  evlsgsummul  22048  evls1gsumadd  22260  evls1gsummul  22261  evl1gsummul  22296  neiptoptop  23067  lpval  23075  neitr  23116  ordtbaslem  23124  ordtrest2  23140  cnrest2  23222  cnpresti  23224  cnprest  23225  cnprest2  23226  connsuba  23356  connsubclo  23360  unconn  23365  1stcelcls  23397  hausmapdom  23436  dissnref  23464  ptbasfi  23517  ptcls  23552  cnmpt2res  23613  qtopval2  23632  elqtop  23633  qtoprest  23653  ptuncnv  23743  ptunhmeo  23744  fsubbas  23803  elfm  23883  rnelfmlem  23888  rnelfm  23889  fmfnfmlem4  23893  flimclslem  23920  hauspwpwdom  23924  ptcmplem1  23988  cnextcn  24003  cnextfres1  24004  isust  24140  trust  24166  elutop  24170  restutop  24174  trcfilu  24230  cfiluweak  24231  psmetres2  24251  xmetres2  24298  fmcfil  25222  dvaddf  25895  dvmulf  25896  dvcmulf  25898  dvcof  25902  ulmss  26356  nosupno  27665  noinfno  27680  sssslt1  27757  sssslt2  27758  sltonex  28201  perpln1  28635  perpln2  28636  isperp  28637  wksfval  29535  fnpreimac  32595  fisuppov1  32606  resf1o  32653  hashpss  32734  gsumpart  32997  gsumwrd2dccat  33007  cycpmco2lem5  33087  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspn  33187  erlval  33199  rlocval  33200  rlocbas  33208  fldgenval  33252  islinds5  33328  ellspds  33329  elrsp  33333  elrspunidl  33389  resssra  33573  lbslelsp  33583  lbsdiflsp0  33612  irngval  33672  ordtrest2NEW  33900  lmlim  33924  esummono  34031  esumrnmpt2  34045  esumpinfval  34050  elcarsg  34283  carsgmon  34292  carsggect  34296  reprval  34588  repr0  34589  reprsuc  34593  reprss  34595  reprinrn  34596  reprlt  34597  reprgt  34599  reprinfz1  34600  reprpmtf1o  34604  reprdifc  34605  bnj1413  35012  cvmliftmolem1  35249  satf0suclem  35343  fwddifval  36126  neibastop1  36323  neibastop2lem  36324  fnejoin1  36332  filnetlem3  36344  filnetlem4  36345  weiunse  36432  numiunnum  36434  bj-imdirval2lem  37146  bj-imdirval3  37148  bj-imdirco  37154  dissneqlem  37304  aks6d1c2lem4  42086  sticksstones20  42125  aks6d1c6lem3  42131  psrbagres  42516  selvcllemh  42550  selvcllem4  42551  selvcllem5  42552  selvcl  42553  selvval2  42554  selvvvval  42555  evlselv  42557  selvadd  42558  selvmul  42559  fsuppssindlem2  42562  fsuppssind  42563  elrfi  42664  elrfirn2  42666  oaun3lem3  43347  nadd2rabex  43357  clcnvlem  43594  relexpss1d  43676  k0004lem2  44119  ixpssmapc  45045  restuni4  45093  restsubel  45125  wessf1ornlem  45157  disjinfi  45164  unirnmap  45180  inmap  45181  difmapsn  45184  unirnmapsn  45186  ssmapsn  45188  limsupre  45618  limsuppnfdlem  45678  limsuppnflem  45687  limsupmnflem  45697  limsupre2lem  45701  liminfval4  45766  liminfval3  45767  icccncfext  45864  dvdivcncf  45904  dvnprodlem1  45923  dvnprodlem2  45924  ovolsplit  45965  stoweidlem31  46008  stoweidlem53  46030  stoweidlem57  46034  stoweidlem59  46036  etransclem46  46257  salexct  46311  subsaluni  46337  fsumlesge0  46354  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  meadjuni  46434  meadjiunlem  46442  omessle  46475  omecl  46480  isomenndlem  46507  caragencmpl  46512  ovnval2  46522  ovnval2b  46529  ovncvrrp  46541  ovncl  46544  hoidmvlelem2  46573  hoidmvlelem3  46574  ovncvr2  46588  ovnsubadd2lem  46622  ovnovollem3  46635  vonvolmbllem  46637  vonvolmbl  46638  sssmf  46715  incsmf  46719  issmflelem  46721  issmfle  46722  smfconst  46726  issmfgtlem  46732  issmfgt  46733  smfaddlem2  46741  decsmf  46744  issmfgelem  46746  issmfge  46747  nsssmfmbflem  46755  smfpimioo  46764  smfresal  46765  smfmullem4  46771  smfpimbor1lem1  46775  smf2id  46778  upwlksfval  48058  toplatglb  48923