Theorem ssv 3963

Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.)

Assertion

Ref	Expression
ssv	⊢ 𝐴 ⊆ V

Proof of Theorem ssv

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3478	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3943	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3457   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924

This theorem is referenced by:  inv1  4355  unv  4356  vss  4403  pssv  4406  disj2  4415  pwv  4864  unissint  4932  symdifv  5047  trv  5225  intabs  5309  xpss  5667  inxpssres  5668  djussxp  5821  dmv  5902  dmresi  6044  cnvrescnv  6185  rescnvcnv  6194  cocnvcnv1  6248  relrelss  6263  fnresi  6654  dffn2  6697  oprabss  7508  fvresex  7945  ofmres  7969  f1stres  7998  f2ndres  7999  fsplitfpar  8101  domssex2  9113  fineqv  9215  fiint  9274  marypha1lem  9381  marypha2  9387  cantnfval2  9626  cottrcl  9676  inlresf1  9889  inrresf1  9891  djuun  9900  dfac12lem2  10116  dfac12a  10120  fin23lem41  10324  dfacfin7  10371  iunfo  10511  gch2  10648  axpre-sup  11142  wrdv  14554  setscom  17228  isofn  17820  homaf  18075  dmaf  18094  cdaf  18095  prdsinvlem  19103  frgpuplem  19830  gsum2dlem2  20029  gsum2d  20030  prdsmgp  20215  rngmgpf  20223  mgpf  20318  prdscrngd  20391  pws1  20394  mulgass3  20423  crngridl  21378  frlmbas  21862  islindf3  21933  psdmul  22286  ply1lss  22313  coe1fval3  22325  coe1tm  22391  ply1coe  22415  evl1expd  22462  pmatcollpw3lem  22897  clsconn  23544  ptbasfi  23695  upxp  23737  uptx  23739  prdstps  23743  hausdiag  23759  cnmpt1st  23782  cnmpt2nd  23783  fbssint  23952  prdstmdd  24238  prdsxmslem2  24643  isngp2  24711  uniiccdif  25694  wlkdlem1  29935  0vfval  30863  xppreima  32898  2ndimaxp  32899  2ndresdju  32902  xppreima2  32904  1stpreimas  32959  fsuppcurry1  32977  fsuppcurry2  32978  ffsrn  32981  gsummpt2d  33277  gsumpart  33291  elrgspnlem2  33471  lindflbs  33603  elrspunidl  33647  dimval  33903  dimvalfi  33904  qtophaus  34138  cnre2csqlem  34212  cntmeas  34528  eulerpartlemmf  34677  eulerpartlemgf  34681  sseqfv1  34691  sseqfn  34692  sseqfv2  34696  coinflippv  34786  fineqvacALT  35420  gblacfnacd  35452  vonf1wev  35458  vonf1owevOLD  35460  wevgblacfn  35461  wevonprcf1o  35463  vonf1oonf1  35464  erdszelem2  35550  mpstssv  35897  filnetlem4  36749  regsfromunir1  36908  bj-0int  37598  bj-idres  37659  elxp8  37872  poimirlem26  38152  poimirlem27  38153  heibor1lem  38315  dmsucmap  38974  isnumbasgrplem1  43685  isnumbasgrplem2  43688  dfacbasgrp  43692  resnonrel  44175  comptiunov2i  44289  ntrneiel2  44669  ntrneik4w  44683  conss2  45011  permaxun  45579  permac8prim  45582  slotresfo  49529  basresposfo  49608  ipoglb0  49624  mreclat  49627  isofnALT  49661  rescofuf  49723  initopropdlem  49870  termopropdlem  49871  zeroopropdlem  49872