Theorem ssexd 5030

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

Syntax hints:   → wi 4   ∈ wcel 2166  Vcvv 3414   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803  ax-sep 5005

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-in 3805  df-ss 3812

This theorem is referenced by:  sselpwd  5032  opabbrex  6955  soex  7371  fex2  7383  opabex2  7489  fnwelem  7556  fnse  7558  extmptsuppeq  7583  f1imaen2g  8283  ordtypelem10  8701  oismo  8714  wofib  8719  wemapso  8725  wdom2d  8754  wdomd  8755  unxpwdom2  8762  cantnfle  8845  cantnflt  8846  cantnflt2  8847  cantnfp1lem2  8853  cantnfp1lem3  8854  cantnflem1b  8860  cantnflem1d  8862  cnfcom  8874  cnfcom2lem  8875  djuexALT  9061  acni2  9182  fin1a2lem12  9548  hsmexlem1  9563  zorn2lem4  9636  fpwwe2lem2  9769  fpwwe2lem5  9771  fpwwe2lem12  9778  fpwwe2  9780  fpwwelem  9782  canthwelem  9787  pwfseqlem4  9799  trclfv  14118  hashbcss  16079  strssd  16272  restid2  16444  divsfval  16560  mrieqv2d  16652  mrissmrcd  16653  mreexexlemd  16657  mreexexlem3d  16659  mreexexlem4d  16660  mreexdomd  16662  rescabs  16845  rescabs2  16846  resssetc  17094  resscatc  17107  estrresOLD  17131  estrres  17132  yonedalem1  17265  yonedalem21  17266  yonedalem3a  17267  yonedalem4c  17270  yonedalem22  17271  yonedalem3b  17272  yonedainv  17274  yonffthlem  17275  joinfval  17354  meetfval  17368  acsdomd  17534  gass  18084  pmtrfconj  18236  sylow2blem2  18387  dprdres  18781  dmdprdsplitlem  18790  pwssplit0  19417  pwssplit1  19418  pwssplit2  19419  pwssplit3  19420  opsrtoslem2  19845  evls1gsumadd  20049  evls1gsummul  20050  evl1gsummul  20084  frlmsplit2  20479  frlmsslss  20480  neiptoptop  21306  lpval  21314  neitr  21355  ordtbaslem  21363  ordtrest2  21379  cnrest2  21461  cnpresti  21463  cnprest  21464  cnprest2  21465  connsuba  21594  connsubclo  21598  unconn  21603  1stcelcls  21635  hausmapdom  21674  dissnref  21702  ptbasfi  21755  ptcls  21790  cnmpt2res  21851  qtopval2  21870  elqtop  21871  qtoprest  21891  ptuncnv  21981  ptunhmeo  21982  fsubbas  22041  elfm  22121  rnelfmlem  22126  rnelfm  22127  fmfnfmlem4  22131  flimclslem  22158  hauspwpwdom  22162  ptcmplem1  22226  cnextcn  22241  cnextfres1  22242  isust  22377  trust  22403  elutop  22407  restutop  22411  trcfilu  22468  cfiluweak  22469  psmetres2  22489  xmetres2  22536  fmcfil  23440  dvnf  24089  dvnbss  24090  dvaddf  24104  dvmulf  24105  dvcmulf  24107  dvcof  24110  ulmss  24550  perpln1  26022  perpln2  26023  isperp  26024  wksfval  26907  resf1o  30053  ordtrest2NEW  30514  lmlim  30538  esummono  30661  esumrnmpt2  30675  esumpinfval  30680  carsgmon  30921  carsggect  30925  reprval  31237  repr0  31238  reprsuc  31242  reprss  31244  reprinrn  31245  reprlt  31246  reprgt  31248  reprinfz1  31249  reprpmtf1o  31253  reprdifc  31254  bnj1413  31649  cvmliftmolem1  31809  nosupno  32388  sssslt1  32445  sssslt2  32446  fwddifval  32808  neibastop1  32892  neibastop2lem  32893  fnejoin1  32901  filnetlem3  32913  filnetlem4  32914  dissneqlem  33733  elrfi  38101  elrfirn2  38103  clcnvlem  38771  relexpss1d  38838  k0004lem2  39286  ixpssmapc  40060  restuni4  40119  wessf1ornlem  40179  unirnmap  40206  inmap  40207  difmapsn  40210  unirnmapsn  40212  ssmapsn  40214  limsupre  40668  limsuppnfdlem  40728  limsuppnflem  40737  limsupmnflem  40747  limsupre2lem  40751  liminfval4  40816  liminfval3  40817  icccncfext  40895  dvdivcncf  40937  dvnprodlem1  40956  dvnprodlem2  40957  ovolsplit  40999  stoweidlem31  41042  stoweidlem53  41064  stoweidlem57  41068  stoweidlem59  41070  etransclem46  41291  saliuncl  41333  salexct  41343  subsaluni  41369  fsumlesge0  41385  sge0f1o  41390  sge0iunmptlemfi  41421  sge0iunmptlemre  41423  meadjuni  41465  meadjiunlem  41473  omessle  41506  omecl  41511  isomenndlem  41538  caragencmpl  41543  ovnval2  41553  ovnval2b  41560  ovncvrrp  41572  ovncl  41575  hoidmvlelem2  41604  hoidmvlelem3  41605  ovncvr2  41619  ovnsubadd2lem  41653  ovnovollem3  41666  vonvolmbllem  41668  vonvolmbl  41669  sssmf  41741  incsmf  41745  issmflelem  41747  issmfle  41748  smfconst  41752  issmfgtlem  41758  issmfgt  41759  smfaddlem2  41766  decsmf  41769  issmfgelem  41771  issmfge  41772  nsssmfmbflem  41780  smfpimioo  41788  smfresal  41789  smfmullem4  41795  smfpimbor1lem1  41799  smf2id  41802  upwlksfval  42563