Theorem ssv 3946

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

Syntax hints:  Vcvv 3432   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907

This theorem is referenced by:  inv1  4333  unv  4334  vss  4381  pssv  4384  disj2  4393  pwv  4842  unissint  4909  symdifv  5022  trv  5200  intabs  5284  xpss  5641  inxpssres  5642  djussxp  5794  dmv  5871  dmresi  6011  cnvrescnv  6153  rescnvcnv  6162  cocnvcnv1  6216  relrelss  6231  fnresi  6621  dffn2  6664  oprabss  7471  fvresex  7909  ofmres  7933  f1stres  7962  f2ndres  7963  fsplitfpar  8064  domssex2  9072  fineqv  9174  fiint  9234  marypha1lem  9343  marypha2  9349  cantnfval2  9588  cottrcl  9638  inlresf1  9837  inrresf1  9839  djuun  9848  dfac12lem2  10065  dfac12a  10069  fin23lem41  10272  dfacfin7  10319  iunfo  10459  gch2  10596  axpre-sup  11090  wrdv  14489  setscom  17148  isofn  17740  homaf  17995  dmaf  18014  cdaf  18015  prdsinvlem  19023  frgpuplem  19745  gsum2dlem2  19944  gsum2d  19945  prdsmgp  20130  rngmgpf  20136  mgpf  20227  prdscrngd  20299  pws1  20302  mulgass3  20331  crngridl  21280  frlmbas  21737  islindf3  21808  psdmul  22161  ply1lss  22188  coe1fval3  22200  coe1tm  22266  ply1coe  22291  evl1expd  22338  pmatcollpw3lem  22773  clsconn  23420  ptbasfi  23571  upxp  23613  uptx  23615  prdstps  23619  hausdiag  23635  cnmpt1st  23658  cnmpt2nd  23659  fbssint  23828  prdstmdd  24114  prdsxmslem2  24519  isngp2  24587  uniiccdif  25570  wlkdlem1  29774  0vfval  30702  xppreima  32744  2ndimaxp  32745  2ndresdju  32748  xppreima2  32750  1stpreimas  32805  fsuppcurry1  32823  fsuppcurry2  32824  ffsrn  32827  gsummpt2d  33137  gsumpart  33151  elrgspnlem2  33331  lindflbs  33469  elrspunidl  33518  dimval  33792  dimvalfi  33793  qtophaus  34027  cnre2csqlem  34101  cntmeas  34417  eulerpartlemmf  34566  eulerpartlemgf  34570  sseqfv1  34580  sseqfn  34581  sseqfv2  34585  coinflippv  34675  fineqvacALT  35305  gblacfnacd  35337  vonf1owev  35343  wevgblacfn  35344  erdszelem2  35427  mpstssv  35774  filnetlem4  36616  regsfromunir1  36775  bj-0int  37466  bj-idres  37527  elxp8  37740  poimirlem26  38020  poimirlem27  38021  heibor1lem  38183  dmsucmap  38842  isnumbasgrplem1  43553  isnumbasgrplem2  43556  dfacbasgrp  43560  resnonrel  44043  comptiunov2i  44157  ntrneiel2  44537  ntrneik4w  44551  conss2  44893  permaxun  45462  permac8prim  45465  slotresfo  49396  basresposfo  49475  ipoglb0  49491  mreclat  49494  isofnALT  49528  rescofuf  49590  initopropdlem  49737  termopropdlem  49738  zeroopropdlem  49739