Theorem ssv 3988

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

Syntax hints:  Vcvv 3464   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948

This theorem is referenced by:  inv1  4378  unv  4379  vss  4426  pssv  4429  disj2  4438  pwv  4885  unissint  4953  symdifv  5067  trv  5248  intabs  5324  xpss  5675  inxpssres  5676  djussxp  5830  dmv  5907  dmresi  6044  cnvrescnv  6189  rescnvcnv  6198  cocnvcnv1  6251  relrelss  6267  fnresi  6672  dffn2  6713  oprabss  7520  fvresex  7963  ofmres  7988  f1stres  8017  f2ndres  8018  fsplitfpar  8122  domssex2  9156  fineqv  9276  fiint  9343  fiintOLD  9344  marypha1lem  9450  marypha2  9456  cantnfval2  9688  cottrcl  9738  inlresf1  9934  inrresf1  9936  djuun  9945  dfac12lem2  10164  dfac12a  10168  fin23lem41  10371  dfacfin7  10418  iunfo  10558  gch2  10694  axpre-sup  11188  wrdv  14552  setscom  17204  isofn  17793  homaf  18048  dmaf  18067  cdaf  18068  prdsinvlem  19037  frgpuplem  19758  gsum2dlem2  19957  gsum2d  19958  prdsmgp  20116  rngmgpf  20122  mgpf  20213  prdscrngd  20287  pws1  20290  mulgass3  20318  crngridl  21246  frlmbas  21720  islindf3  21791  psdmul  22109  ply1lss  22137  coe1fval3  22149  coe1tm  22215  ply1coe  22241  evl1expd  22288  pmatcollpw3lem  22726  clsconn  23373  ptbasfi  23524  upxp  23566  uptx  23568  prdstps  23572  hausdiag  23588  cnmpt1st  23611  cnmpt2nd  23612  fbssint  23781  prdstmdd  24067  prdsxmslem2  24473  isngp2  24541  uniiccdif  25536  wlkdlem1  29667  0vfval  30592  xppreima  32628  2ndimaxp  32629  2ndresdju  32632  xppreima2  32634  1stpreimas  32688  fsuppcurry1  32707  fsuppcurry2  32708  ffsrn  32711  gsummpt2d  33048  gsumpart  33056  elrgspnlem2  33243  lindflbs  33399  elrspunidl  33448  dimval  33645  dimvalfi  33646  qtophaus  33872  cnre2csqlem  33946  cntmeas  34262  eulerpartlemmf  34412  eulerpartlemgf  34416  sseqfv1  34426  sseqfn  34427  sseqfv2  34431  coinflippv  34521  fineqvacALT  35134  gblacfnacd  35135  wevgblacfn  35136  erdszelem2  35219  mpstssv  35566  filnetlem4  36404  bj-0int  37124  bj-idres  37183  elxp8  37394  poimirlem26  37675  poimirlem27  37676  heibor1lem  37838  rmxyelqirrOLD  42909  isnumbasgrplem1  43100  isnumbasgrplem2  43103  dfacbasgrp  43107  resnonrel  43591  comptiunov2i  43705  ntrneiel2  44085  ntrneik4w  44099  conss2  44442  permaxun  45011  permac8prim  45014  slotresfo  48853  basresposfo  48932  ipoglb0  48948  mreclat  48951  isofnALT  48981  rescofuf  49036  initopropdlem  49137  termopropdlem  49138  zeroopropdlem  49139