Theorem ssexd 5192

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sselpwd  5194  opabbrex  7186  soex  7608  fex2  7620  funexw  7635  opabex2  7737  fnwelem  7808  fnse  7810  extmptsuppeq  7837  f1imaen2g  8553  ordtypelem10  8975  oismo  8988  wofib  8993  wemapso  8999  wdom2d  9028  wdomd  9029  unxpwdom2  9036  djuexALT  9335  acni2  9457  fin1a2lem12  9822  hsmexlem1  9837  zorn2lem4  9910  fpwwe2lem2  10043  fpwwe2lem5  10045  fpwwe2lem12  10052  fpwwe2  10054  fpwwelem  10056  canthwelem  10061  pwfseqlem4  10073  trclfv  14351  hashbcss  16330  strssd  16525  restid2  16696  divsfval  16812  mrieqv2d  16902  mrissmrcd  16903  mreexexlemd  16907  mreexexlem3d  16909  mreexexlem4d  16910  mreexdomd  16912  rescabs  17095  rescabs2  17096  resssetc  17344  resscatc  17357  estrres  17381  yonedalem1  17514  yonedalem21  17515  yonedalem3a  17516  yonedalem4c  17519  yonedalem22  17520  yonedalem3b  17521  yonedainv  17523  yonffthlem  17524  joinfval  17603  meetfval  17617  acsdomd  17783  gass  18423  permsetex  18490  pmtrfconj  18586  sylow2blem2  18738  dprdres  19143  dmdprdsplitlem  19152  primefld  19577  pwssplit0  19823  pwssplit1  19824  pwssplit2  19825  pwssplit3  19826  frlmsplit2  20462  frlmsslss  20463  opsrtoslem2  20724  evlsgsumadd  20763  evlsgsummul  20764  evls1gsumadd  20948  evls1gsummul  20949  evl1gsummul  20984  neiptoptop  21736  lpval  21744  neitr  21785  ordtbaslem  21793  ordtrest2  21809  cnrest2  21891  cnpresti  21893  cnprest  21894  cnprest2  21895  connsuba  22025  connsubclo  22029  unconn  22034  1stcelcls  22066  hausmapdom  22105  dissnref  22133  ptbasfi  22186  ptcls  22221  cnmpt2res  22282  qtopval2  22301  elqtop  22302  qtoprest  22322  ptuncnv  22412  ptunhmeo  22413  fsubbas  22472  elfm  22552  rnelfmlem  22557  rnelfm  22558  fmfnfmlem4  22562  flimclslem  22589  hauspwpwdom  22593  ptcmplem1  22657  cnextcn  22672  cnextfres1  22673  isust  22809  trust  22835  elutop  22839  restutop  22843  trcfilu  22900  cfiluweak  22901  psmetres2  22921  xmetres2  22968  fmcfil  23876  dvaddf  24545  dvmulf  24546  dvcmulf  24548  dvcof  24551  ulmss  24992  perpln1  26504  perpln2  26505  isperp  26506  wksfval  27399  fnpreimac  30434  resf1o  30492  gsumpart  30740  cycpmco2lem5  30822  islinds5  30983  ellspds  30984  elrsp  30989  elrspunidl  31014  lbsdiflsp0  31110  ordtrest2NEW  31276  lmlim  31300  esummono  31423  esumrnmpt2  31437  esumpinfval  31442  elcarsg  31673  carsgmon  31682  carsggect  31686  reprval  31991  repr0  31992  reprsuc  31996  reprss  31998  reprinrn  31999  reprlt  32000  reprgt  32002  reprinfz1  32003  reprpmtf1o  32007  reprdifc  32008  bnj1413  32417  cvmliftmolem1  32641  satf0suclem  32735  nosupno  33316  sssslt1  33373  sssslt2  33374  fwddifval  33736  neibastop1  33820  neibastop2lem  33821  fnejoin1  33829  filnetlem3  33841  filnetlem4  33842  bj-imdirval2lem  34597  bj-imdirval3  34599  bj-imdirco  34605  dissneqlem  34757  selvval2lemn  39430  selvval2lem4  39431  selvval2lem5  39432  selvcl  39433  fsuppssindlem2  39458  fsuppssind  39459  elrfi  39635  elrfirn2  39637  clcnvlem  40323  relexpss1d  40406  k0004lem2  40851  ixpssmapc  41708  restuni4  41756  wessf1ornlem  41811  disjinfi  41820  unirnmap  41837  inmap  41838  difmapsn  41841  unirnmapsn  41843  ssmapsn  41845  limsupre  42283  limsuppnfdlem  42343  limsuppnflem  42352  limsupmnflem  42362  limsupre2lem  42366  liminfval4  42431  liminfval3  42432  icccncfext  42529  dvdivcncf  42569  dvnprodlem1  42588  dvnprodlem2  42589  ovolsplit  42630  stoweidlem31  42673  stoweidlem53  42695  stoweidlem57  42699  stoweidlem59  42701  etransclem46  42922  saliuncl  42964  salexct  42974  subsaluni  43000  fsumlesge0  43016  sge0f1o  43021  sge0iunmptlemfi  43052  sge0iunmptlemre  43054  meadjuni  43096  meadjiunlem  43104  omessle  43137  omecl  43142  isomenndlem  43169  caragencmpl  43174  ovnval2  43184  ovnval2b  43191  ovncvrrp  43203  ovncl  43206  hoidmvlelem2  43235  hoidmvlelem3  43236  ovncvr2  43250  ovnsubadd2lem  43284  ovnovollem3  43297  vonvolmbllem  43299  vonvolmbl  43300  sssmf  43372  incsmf  43376  issmflelem  43378  issmfle  43379  smfconst  43383  issmfgtlem  43389  issmfgt  43390  smfaddlem2  43397  decsmf  43400  issmfgelem  43402  issmfge  43403  nsssmfmbflem  43411  smfpimioo  43419  smfresal  43420  smfmullem4  43426  smfpimbor1lem1  43430  smf2id  43433  upwlksfval  44363