Theorem ssexd 5249

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433   ⊆ wss 3888

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 2710  ax-sep 5224

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sselpwd  5251  opabbrex  7335  soex  7777  fex2  7789  funexw  7803  opabex2  7906  fnwelem  7981  fnse  7983  extmptsuppeq  8013  f1setex  8654  f1imaen2g  8810  ordtypelem10  9295  oismo  9308  wofib  9313  wdom2d  9348  wdomd  9349  unxpwdom2  9356  ttrclexg  9490  djuexALT  9689  acni2  9811  fin1a2lem12  10176  hsmexlem1  10191  zorn2lem4  10264  fpwwe2lem2  10397  fpwwe2lem4  10399  fpwwe2lem11  10406  fpwwe2  10408  fpwwelem  10410  canthwelem  10415  pwfseqlem4  10427  hashf1lem1  14177  trclfv  14720  hashbcss  16714  strssd  16916  restid2  17150  divsfval  17267  mrieqv2d  17357  mrissmrcd  17358  mreexexlemd  17362  mreexexlem3d  17364  mreexexlem4d  17365  mreexdomd  17367  rescabs  17556  rescabsOLD  17557  rescabs2  17558  resssetc  17816  resscatc  17833  estrres  17865  yonedalem1  17999  yonedalem21  18000  yonedalem3a  18001  yonedalem4c  18004  yonedalem22  18005  yonedalem3b  18006  yonedainv  18008  yonffthlem  18009  joinfval  18100  meetfval  18114  acsdomd  18284  gass  18916  permsetexOLD  18986  pmtrfconj  19083  sylow2blem2  19235  dprdres  19640  dmdprdsplitlem  19649  primefld  20082  pwssplit0  20329  pwssplit1  20330  pwssplit2  20331  pwssplit3  20332  frlmsplit2  20989  frlmsslss  20990  opsrtoslem2  21272  evlsgsumadd  21310  evlsgsummul  21311  evls1gsumadd  21499  evls1gsummul  21500  evl1gsummul  21535  neiptoptop  22291  lpval  22299  neitr  22340  ordtbaslem  22348  ordtrest2  22364  cnrest2  22446  cnpresti  22448  cnprest  22449  cnprest2  22450  connsuba  22580  connsubclo  22584  unconn  22589  1stcelcls  22621  hausmapdom  22660  dissnref  22688  ptbasfi  22741  ptcls  22776  cnmpt2res  22837  qtopval2  22856  elqtop  22857  qtoprest  22877  ptuncnv  22967  ptunhmeo  22968  fsubbas  23027  elfm  23107  rnelfmlem  23112  rnelfm  23113  fmfnfmlem4  23117  flimclslem  23144  hauspwpwdom  23148  ptcmplem1  23212  cnextcn  23227  cnextfres1  23228  isust  23364  trust  23390  elutop  23394  restutop  23398  trcfilu  23455  cfiluweak  23456  psmetres2  23476  xmetres2  23523  fmcfil  24445  dvaddf  25115  dvmulf  25116  dvcmulf  25118  dvcof  25121  ulmss  25565  perpln1  27080  perpln2  27081  isperp  27082  wksfval  27985  fnpreimac  31017  resf1o  31074  gsumpart  31324  cycpmco2lem5  31406  islinds5  31572  ellspds  31573  elrsp  31578  elrspunidl  31615  lbsdiflsp0  31716  ordtrest2NEW  31882  lmlim  31906  esummono  32031  esumrnmpt2  32045  esumpinfval  32050  elcarsg  32281  carsgmon  32290  carsggect  32294  reprval  32599  repr0  32600  reprsuc  32604  reprss  32606  reprinrn  32607  reprlt  32608  reprgt  32610  reprinfz1  32611  reprpmtf1o  32615  reprdifc  32616  bnj1413  33024  cvmliftmolem1  33252  satf0suclem  33346  nosupno  33915  noinfno  33930  sssslt1  33998  sssslt2  33999  fwddifval  34473  neibastop1  34557  neibastop2lem  34558  fnejoin1  34566  filnetlem3  34578  filnetlem4  34579  bj-imdirval2lem  35362  bj-imdirval3  35364  bj-imdirco  35370  dissneqlem  35520  sticksstones20  40129  selvval2lemn  40234  selvval2lem4  40235  selvval2lem5  40236  selvcl  40237  fsuppssindlem2  40288  fsuppssind  40289  elrfi  40523  elrfirn2  40525  clcnvlem  41238  relexpss1d  41320  k0004lem2  41765  ixpssmapc  42629  restuni4  42677  wessf1ornlem  42729  disjinfi  42738  unirnmap  42755  inmap  42756  difmapsn  42759  unirnmapsn  42761  ssmapsn  42763  limsupre  43189  limsuppnfdlem  43249  limsuppnflem  43258  limsupmnflem  43268  limsupre2lem  43272  liminfval4  43337  liminfval3  43338  icccncfext  43435  dvdivcncf  43475  dvnprodlem1  43494  dvnprodlem2  43495  ovolsplit  43536  stoweidlem31  43579  stoweidlem53  43601  stoweidlem57  43605  stoweidlem59  43607  etransclem46  43828  saliuncl  43870  salexct  43880  subsaluni  43906  fsumlesge0  43922  sge0f1o  43927  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  meadjuni  44002  meadjiunlem  44010  omessle  44043  omecl  44048  isomenndlem  44075  caragencmpl  44080  ovnval2  44090  ovnval2b  44097  ovncvrrp  44109  ovncl  44112  hoidmvlelem2  44141  hoidmvlelem3  44142  ovncvr2  44156  ovnsubadd2lem  44190  ovnovollem3  44203  vonvolmbllem  44205  vonvolmbl  44206  sssmf  44283  incsmf  44287  issmflelem  44289  issmfle  44290  smfconst  44294  issmfgtlem  44300  issmfgt  44301  smfaddlem2  44309  decsmf  44312  issmfgelem  44314  issmfge  44315  nsssmfmbflem  44323  smfpimioo  44332  smfresal  44333  smfmullem4  44339  smfpimbor1lem1  44343  smf2id  44346  upwlksfval  45308  toplatglb  46298