Theorem ssexd 5295

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423  df-v 3463  df-in 3918  df-ss 3928

This theorem is referenced by:  abexd  5296  sselpwd  5299  sepab  5303  moabex  5440  opabbrex  7464  soex  7918  fex2  7933  fabexd  7934  mapex  7937  funexw  7949  opabex2  8054  fnwelem  8127  fnse  8129  extmptsuppeq  8184  f1setex  8854  f1imaen2g  9012  fsuppss  9343  ordtypelem10  9489  oismo  9502  wofib  9507  wdom2d  9542  wdomd  9543  unxpwdom2  9550  ttrclexg  9692  djuexALT  9908  acni2  10030  fin1a2lem12  10395  hsmexlem1  10410  zorn2lem4  10483  ondomon  10547  fpwwe2lem2  10617  fpwwe2lem4  10619  fpwwe2lem11  10626  fpwwe2  10628  fpwwelem  10630  canthwelem  10635  pwfseqlem4  10647  hashpss  14446  hashf1lem1  14492  trclfv  15037  hashbcss  17064  strssd  17265  restid2  17483  divsfval  17601  mrieqv2d  17695  mrissmrcd  17696  mreexexlemd  17700  mreexexlem3d  17702  mreexexlem4d  17703  mreexdomd  17705  rescabs  17890  rescabs2  17891  resssetc  18149  resscatc  18166  estrres  18195  yonedalem1  18328  yonedalem21  18329  yonedalem3a  18330  yonedalem4c  18333  yonedalem22  18334  yonedalem3b  18335  yonedainv  18337  yonffthlem  18338  joinfval  18427  meetfval  18441  acsdomd  18613  ressmulgnnd  19144  gass  19371  pmtrfconj  19536  sylow2blem2  19691  dprdres  20100  dmdprdsplitlem  20109  primefld  20886  pwssplit0  21157  pwssplit1  21158  pwssplit2  21159  pwssplit3  21160  frlmsplit2  21892  frlmsslss  21893  psrbagres  22049  opsrtoslem2  22176  evlsgsumadd  22216  evlsgsummul  22217  selvcllemh  22257  selvcllem4  22258  selvcllem5  22259  selvcl  22260  selvval2  22261  selvvvval  22262  selvadd  22263  selvmul  22264  evls1gsumadd  22453  evls1gsummul  22454  evl1gsummul  22489  neiptoptop  23257  lpval  23265  neitr  23306  ordtbaslem  23314  ordtrest2  23330  cnrest2  23412  cnpresti  23414  cnprest  23415  cnprest2  23416  connsuba  23546  connsubclo  23550  unconn  23555  1stcelcls  23587  hausmapdom  23626  dissnref  23654  ptbasfi  23707  ptcls  23742  cnmpt2res  23803  qtopval2  23822  elqtop  23823  qtoprest  23843  ptuncnv  23933  ptunhmeo  23934  fsubbas  23993  elfm  24073  rnelfmlem  24078  rnelfm  24079  fmfnfmlem4  24083  flimclslem  24110  hauspwpwdom  24114  ptcmplem1  24178  cnextcn  24193  cnextfres1  24194  isust  24330  trust  24355  elutop  24359  restutop  24363  trcfilu  24419  cfiluweak  24420  psmetres2  24440  xmetres2  24487  fmcfil  25400  dvaddf  26070  dvmulf  26071  dvcmulf  26073  dvcof  26076  ulmss  26526  nosupno  27833  noinfno  27848  ssslts1  27932  ssslts2  27933  ltonsex  28421  perpln1  28949  perpln2  28950  isperp  28951  wksfval  29900  fnpreimac  32956  fisuppov1  32969  resf1o  33016  gsumpart  33324  gsumwrd2dccat  33339  cycpmco2lem5  33391  elrgspnlem1  33503  elrgspnlem2  33504  elrgspnlem3  33505  elrgspnlem4  33506  elrgspn  33507  erlval  33519  rlocval  33520  rlocbas  33529  fldgenval  33576  islinds5  33625  ellspds  33626  elrsp  33629  elrspunidl  33680  mplasclco  33851  selvascl  33852  evlextv  33877  psrmonprod  33887  esplympl  33902  resssra  33922  lbslelsp  33933  lbsdiflsp0  33961  irngval  34020  ordtrest2NEW  34258  lmlim  34282  esummono  34389  esumrnmpt2  34403  esumpinfval  34408  elcarsg  34640  carsgmon  34649  carsggect  34653  reprval  34942  repr0  34943  reprsuc  34947  reprss  34949  reprinrn  34950  reprlt  34951  reprgt  34953  reprinfz1  34954  reprpmtf1o  34958  reprdifc  34959  bnj1413  35368  cvmliftmolem1  35706  satf0suclem  35800  fwddifval  36587  neibastop1  36793  neibastop2lem  36794  fnejoin1  36802  filnetlem3  36814  filnetlem4  36815  weiunse  36902  numiunnum  36904  bj-imdirval2lem  37749  bj-imdirval3  37751  bj-imdirco  37757  dissneqlem  37909  aks6d1c2lem4  42819  sticksstones20  42858  aks6d1c6lem3  42864  evlselv  43248  fsuppssindlem2  43251  fsuppssind  43252  elrfi  43352  elrfirn2  43354  oaun3lem3  44030  nadd2rabex  44040  clcnvlem  44276  relexpss1d  44358  k0004lem2  44801  ixpssmapc  45720  restuni4  45766  restsubel  45798  wessf1ornlem  45830  disjinfi  45837  unirnmap  45851  inmap  45852  difmapsn  45855  unirnmapsn  45857  ssmapsn  45859  limsupre  46282  limsuppnfdlem  46342  limsuppnflem  46351  limsupmnflem  46361  limsupre2lem  46365  liminfval4  46430  liminfval3  46431  icccncfext  46528  dvdivcncf  46568  dvnprodlem1  46587  dvnprodlem2  46588  ovolsplit  46629  stoweidlem31  46672  stoweidlem53  46694  stoweidlem57  46698  stoweidlem59  46700  etransclem46  46921  salexct  46975  subsaluni  47001  fsumlesge0  47018  sge0iunmptlemfi  47054  sge0iunmptlemre  47056  meadjuni  47098  meadjiunlem  47106  omessle  47139  omecl  47144  isomenndlem  47171  caragencmpl  47176  ovnval2  47186  ovnval2b  47193  ovncvrrp  47205  ovncl  47208  hoidmvlelem2  47237  hoidmvlelem3  47238  ovncvr2  47252  ovnsubadd2lem  47286  ovnovollem3  47299  vonvolmbllem  47301  vonvolmbl  47302  sssmf  47379  incsmf  47383  issmflelem  47385  issmfle  47386  smfconst  47390  issmfgtlem  47396  issmfgt  47397  smfaddlem2  47405  decsmf  47408  issmfgelem  47410  issmfge  47411  nsssmfmbflem  47419  smfpimioo  47428  smfresal  47429  smfmullem4  47435  smfpimbor1lem1  47439  smf2id  47442  upwlksfval  48824  toplatglb  49699