Theorem ssv 3960

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 3463	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3939	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 3442   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920

This theorem is referenced by:  inv1  4352  unv  4353  vss  4400  pssv  4403  disj2  4412  pwv  4862  unissint  4929  symdifv  5043  trv  5220  intabs  5296  xpss  5648  inxpssres  5649  djussxp  5802  dmv  5879  dmresi  6019  cnvrescnv  6161  rescnvcnv  6170  cocnvcnv1  6224  relrelss  6239  fnresi  6629  dffn2  6672  oprabss  7476  fvresex  7914  ofmres  7938  f1stres  7967  f2ndres  7968  fsplitfpar  8070  domssex2  9077  fineqv  9179  fiint  9239  marypha1lem  9348  marypha2  9354  cantnfval2  9590  cottrcl  9640  inlresf1  9839  inrresf1  9841  djuun  9850  dfac12lem2  10067  dfac12a  10071  fin23lem41  10274  dfacfin7  10321  iunfo  10461  gch2  10598  axpre-sup  11092  wrdv  14464  setscom  17119  isofn  17711  homaf  17966  dmaf  17985  cdaf  17986  prdsinvlem  18991  frgpuplem  19713  gsum2dlem2  19912  gsum2d  19913  prdsmgp  20098  rngmgpf  20104  mgpf  20195  prdscrngd  20269  pws1  20272  mulgass3  20301  crngridl  21247  frlmbas  21722  islindf3  21793  psdmul  22121  ply1lss  22149  coe1fval3  22161  coe1tm  22227  ply1coe  22254  evl1expd  22301  pmatcollpw3lem  22739  clsconn  23386  ptbasfi  23537  upxp  23579  uptx  23581  prdstps  23585  hausdiag  23601  cnmpt1st  23624  cnmpt2nd  23625  fbssint  23794  prdstmdd  24080  prdsxmslem2  24485  isngp2  24553  uniiccdif  25547  wlkdlem1  29766  0vfval  30693  xppreima  32734  2ndimaxp  32735  2ndresdju  32738  xppreima2  32740  1stpreimas  32795  fsuppcurry1  32813  fsuppcurry2  32814  ffsrn  32817  gsummpt2d  33142  gsumpart  33156  elrgspnlem2  33336  lindflbs  33471  elrspunidl  33520  dimval  33777  dimvalfi  33778  qtophaus  34013  cnre2csqlem  34087  cntmeas  34403  eulerpartlemmf  34552  eulerpartlemgf  34556  sseqfv1  34566  sseqfn  34567  sseqfv2  34571  coinflippv  34661  fineqvacALT  35292  gblacfnacd  35315  vonf1owev  35321  wevgblacfn  35322  erdszelem2  35405  mpstssv  35752  filnetlem4  36594  regsfromunir1  36689  bj-0int  37351  bj-idres  37412  elxp8  37623  poimirlem26  37894  poimirlem27  37895  heibor1lem  38057  dmsucmap  38716  isnumbasgrplem1  43455  isnumbasgrplem2  43458  dfacbasgrp  43462  resnonrel  43945  comptiunov2i  44059  ntrneiel2  44439  ntrneik4w  44453  conss2  44795  permaxun  45364  permac8prim  45367  slotresfo  49255  basresposfo  49334  ipoglb0  49350  mreclat  49353  isofnALT  49387  rescofuf  49449  initopropdlem  49596  termopropdlem  49597  zeroopropdlem  49598