Theorem ssv 3958

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

Syntax hints:  Vcvv 3453   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919

This theorem is referenced by:  inv1  4349  unv  4350  vss  4397  pssv  4400  disj2  4409  pwv  4859  unissint  4927  symdifv  5040  trv  5218  intabs  5302  xpss  5659  inxpssres  5660  djussxp  5813  dmv  5894  dmresi  6036  cnvrescnv  6176  rescnvcnv  6185  cocnvcnv1  6239  relrelss  6254  fnresi  6644  dffn2  6687  oprabss  7498  fvresex  7935  ofmres  7959  f1stres  7988  f2ndres  7989  fsplitfpar  8090  domssex2  9102  fineqv  9204  fiint  9264  marypha1lem  9372  marypha2  9378  cantnfval2  9617  cottrcl  9667  inlresf1  9866  inrresf1  9868  djuun  9877  dfac12lem2  10094  dfac12a  10098  fin23lem41  10302  dfacfin7  10349  iunfo  10489  gch2  10626  axpre-sup  11120  wrdv  14535  setscom  17206  isofn  17798  homaf  18053  dmaf  18072  cdaf  18073  prdsinvlem  19081  frgpuplem  19802  gsum2dlem2  20001  gsum2d  20002  prdsmgp  20187  rngmgpf  20193  mgpf  20284  prdscrngd  20356  pws1  20359  mulgass3  20388  crngridl  21337  frlmbas  21794  islindf3  21865  psdmul  22218  ply1lss  22245  coe1fval3  22257  coe1tm  22323  ply1coe  22348  evl1expd  22395  pmatcollpw3lem  22830  clsconn  23477  ptbasfi  23628  upxp  23670  uptx  23672  prdstps  23676  hausdiag  23692  cnmpt1st  23715  cnmpt2nd  23716  fbssint  23885  prdstmdd  24171  prdsxmslem2  24576  isngp2  24644  uniiccdif  25627  wlkdlem1  29837  0vfval  30765  xppreima  32807  2ndimaxp  32808  2ndresdju  32811  xppreima2  32813  1stpreimas  32868  fsuppcurry1  32886  fsuppcurry2  32887  ffsrn  32890  gsummpt2d  33189  gsumpart  33203  elrgspnlem2  33384  lindflbs  33525  elrspunidl  33574  dimval  33858  dimvalfi  33859  qtophaus  34093  cnre2csqlem  34167  cntmeas  34483  eulerpartlemmf  34632  eulerpartlemgf  34636  sseqfv1  34646  sseqfn  34647  sseqfv2  34651  coinflippv  34741  fineqvacALT  35373  gblacfnacd  35405  vonf1wev  35411  vonf1owevOLD  35413  wevgblacfn  35414  wevonprcf1o  35416  vonf1oonf1  35417  erdszelem2  35502  mpstssv  35849  filnetlem4  36701  regsfromunir1  36860  bj-0int  37551  bj-idres  37612  elxp8  37825  poimirlem26  38105  poimirlem27  38106  heibor1lem  38268  dmsucmap  38927  isnumbasgrplem1  43638  isnumbasgrplem2  43641  dfacbasgrp  43645  resnonrel  44128  comptiunov2i  44242  ntrneiel2  44622  ntrneik4w  44636  conss2  44978  permaxun  45547  permac8prim  45550  slotresfo  49480  basresposfo  49559  ipoglb0  49575  mreclat  49578  isofnALT  49612  rescofuf  49674  initopropdlem  49821  termopropdlem  49822  zeroopropdlem  49823