Theorem ssexd 5324

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  sselpwd  5326  opabbrex  7457  soex  7909  fex2  7921  funexw  7935  opabex2  8040  fnwelem  8114  fnse  8116  extmptsuppeq  8170  f1setex  8848  f1imaen2g  9008  ordtypelem10  9519  oismo  9532  wofib  9537  wdom2d  9572  wdomd  9573  unxpwdom2  9580  ttrclexg  9715  djuexALT  9914  acni2  10038  fin1a2lem12  10403  hsmexlem1  10418  zorn2lem4  10491  fpwwe2lem2  10624  fpwwe2lem4  10626  fpwwe2lem11  10633  fpwwe2  10635  fpwwelem  10637  canthwelem  10642  pwfseqlem4  10654  hashf1lem1  14412  trclfv  14944  hashbcss  16934  strssd  17136  restid2  17373  divsfval  17490  mrieqv2d  17580  mrissmrcd  17581  mreexexlemd  17585  mreexexlem3d  17587  mreexexlem4d  17588  mreexdomd  17590  rescabs  17779  rescabsOLD  17780  rescabs2  17781  resssetc  18039  resscatc  18056  estrres  18088  yonedalem1  18222  yonedalem21  18223  yonedalem3a  18224  yonedalem4c  18227  yonedalem22  18228  yonedalem3b  18229  yonedainv  18231  yonffthlem  18232  joinfval  18323  meetfval  18337  acsdomd  18507  gass  19160  permsetexOLD  19232  pmtrfconj  19329  sylow2blem2  19484  dprdres  19893  dmdprdsplitlem  19902  primefld  20414  pwssplit0  20662  pwssplit1  20663  pwssplit2  20664  pwssplit3  20665  frlmsplit2  21320  frlmsslss  21321  opsrtoslem2  21609  evlsgsumadd  21646  evlsgsummul  21647  evls1gsumadd  21835  evls1gsummul  21836  evl1gsummul  21871  neiptoptop  22627  lpval  22635  neitr  22676  ordtbaslem  22684  ordtrest2  22700  cnrest2  22782  cnpresti  22784  cnprest  22785  cnprest2  22786  connsuba  22916  connsubclo  22920  unconn  22925  1stcelcls  22957  hausmapdom  22996  dissnref  23024  ptbasfi  23077  ptcls  23112  cnmpt2res  23173  qtopval2  23192  elqtop  23193  qtoprest  23213  ptuncnv  23303  ptunhmeo  23304  fsubbas  23363  elfm  23443  rnelfmlem  23448  rnelfm  23449  fmfnfmlem4  23453  flimclslem  23480  hauspwpwdom  23484  ptcmplem1  23548  cnextcn  23563  cnextfres1  23564  isust  23700  trust  23726  elutop  23730  restutop  23734  trcfilu  23791  cfiluweak  23792  psmetres2  23812  xmetres2  23859  fmcfil  24781  dvaddf  25451  dvmulf  25452  dvcmulf  25454  dvcof  25457  ulmss  25901  nosupno  27196  noinfno  27211  sssslt1  27286  sssslt2  27287  perpln1  27951  perpln2  27952  isperp  27953  wksfval  28856  fnpreimac  31884  resf1o  31943  gsumpart  32195  cycpmco2lem5  32277  fldgenval  32391  islinds5  32469  ellspds  32470  elrsp  32475  elrspunidl  32535  lbsdiflsp0  32700  irngval  32738  ordtrest2NEW  32892  lmlim  32916  esummono  33041  esumrnmpt2  33055  esumpinfval  33060  elcarsg  33293  carsgmon  33302  carsggect  33306  reprval  33611  repr0  33612  reprsuc  33616  reprss  33618  reprinrn  33619  reprlt  33620  reprgt  33622  reprinfz1  33623  reprpmtf1o  33627  reprdifc  33628  bnj1413  34035  cvmliftmolem1  34261  satf0suclem  34355  fwddifval  35123  neibastop1  35233  neibastop2lem  35234  fnejoin1  35242  filnetlem3  35254  filnetlem4  35255  bj-imdirval2lem  36052  bj-imdirval3  36054  bj-imdirco  36060  dissneqlem  36210  sticksstones20  40971  fsuppss  41063  psrbagres  41113  selvcllemh  41150  selvcllem4  41151  selvcllem5  41152  selvcl  41153  selvval2  41154  selvvvval  41155  evlselv  41157  selvadd  41158  selvmul  41159  fsuppssindlem2  41162  fsuppssind  41163  elrfi  41418  elrfirn2  41420  oaun3lem3  42112  nadd2rabex  42122  clcnvlem  42360  relexpss1d  42442  k0004lem2  42885  ixpssmapc  43747  restuni4  43796  restsubel  43833  wessf1ornlem  43868  disjinfi  43877  unirnmap  43893  inmap  43894  difmapsn  43897  unirnmapsn  43899  ssmapsn  43901  limsupre  44344  limsuppnfdlem  44404  limsuppnflem  44413  limsupmnflem  44423  limsupre2lem  44427  liminfval4  44492  liminfval3  44493  icccncfext  44590  dvdivcncf  44630  dvnprodlem1  44649  dvnprodlem2  44650  ovolsplit  44691  stoweidlem31  44734  stoweidlem53  44756  stoweidlem57  44760  stoweidlem59  44762  etransclem46  44983  salexct  45037  subsaluni  45063  fsumlesge0  45080  sge0f1o  45085  sge0iunmptlemfi  45116  sge0iunmptlemre  45118  meadjuni  45160  meadjiunlem  45168  omessle  45201  omecl  45206  isomenndlem  45233  caragencmpl  45238  ovnval2  45248  ovnval2b  45255  ovncvrrp  45267  ovncl  45270  hoidmvlelem2  45299  hoidmvlelem3  45300  ovncvr2  45314  ovnsubadd2lem  45348  ovnovollem3  45361  vonvolmbllem  45363  vonvolmbl  45364  sssmf  45441  incsmf  45445  issmflelem  45447  issmfle  45448  smfconst  45452  issmfgtlem  45458  issmfgt  45459  smfaddlem2  45467  decsmf  45470  issmfgelem  45472  issmfge  45473  nsssmfmbflem  45481  smfpimioo  45490  smfresal  45491  smfmullem4  45497  smfpimbor1lem1  45501  smf2id  45504  upwlksfval  46500  toplatglb  47580