Theorem ssv 4007

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

Syntax hints:  Vcvv 3479   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967

This theorem is referenced by:  inv1  4397  unv  4398  vss  4445  pssv  4448  disj2  4457  pwv  4903  unissint  4971  symdifv  5085  trv  5272  intabs  5348  xpss  5700  inxpssres  5701  djussxp  5855  dmv  5932  dmresi  6069  cnvrescnv  6214  rescnvcnv  6223  cocnvcnv1  6276  relrelss  6292  fnresi  6696  dffn2  6737  oprabss  7542  fvresex  7985  ofmres  8010  f1stres  8039  f2ndres  8040  fsplitfpar  8144  domssex2  9178  fineqv  9300  fiint  9367  fiintOLD  9368  marypha1lem  9474  marypha2  9480  cantnfval2  9710  cottrcl  9760  inlresf1  9956  inrresf1  9958  djuun  9967  dfac12lem2  10186  dfac12a  10190  fin23lem41  10393  dfacfin7  10440  iunfo  10580  gch2  10716  axpre-sup  11210  wrdv  14568  setscom  17218  isofn  17820  homaf  18076  dmaf  18095  cdaf  18096  prdsinvlem  19068  frgpuplem  19791  gsum2dlem2  19990  gsum2d  19991  prdsmgp  20149  rngmgpf  20155  mgpf  20246  prdscrngd  20320  pws1  20323  mulgass3  20354  crngridl  21291  frlmbas  21776  islindf3  21847  psdmul  22171  ply1lss  22199  coe1fval3  22211  coe1tm  22277  ply1coe  22303  evl1expd  22350  pmatcollpw3lem  22790  clsconn  23439  ptbasfi  23590  upxp  23632  uptx  23634  prdstps  23638  hausdiag  23654  cnmpt1st  23677  cnmpt2nd  23678  fbssint  23847  prdstmdd  24133  prdsxmslem2  24543  isngp2  24611  uniiccdif  25614  wlkdlem1  29701  0vfval  30626  xppreima  32656  2ndimaxp  32657  2ndresdju  32660  xppreima2  32662  1stpreimas  32716  fsuppcurry1  32737  fsuppcurry2  32738  ffsrn  32741  gsummpt2d  33053  gsumpart  33061  elrgspnlem2  33248  lindflbs  33408  elrspunidl  33457  dimval  33652  dimvalfi  33653  qtophaus  33836  cnre2csqlem  33910  cntmeas  34228  eulerpartlemmf  34378  eulerpartlemgf  34382  sseqfv1  34392  sseqfn  34393  sseqfv2  34397  coinflippv  34487  fineqvacALT  35113  gblacfnacd  35114  wevgblacfn  35115  erdszelem2  35198  mpstssv  35545  filnetlem4  36383  bj-0int  37103  bj-idres  37162  elxp8  37373  poimirlem26  37654  poimirlem27  37655  heibor1lem  37817  rmxyelqirrOLD  42927  isnumbasgrplem1  43118  isnumbasgrplem2  43121  dfacbasgrp  43125  resnonrel  43610  comptiunov2i  43724  ntrneiel2  44104  ntrneik4w  44118  conss2  44467  slotresfo  48803  basresposfo  48882  ipoglb0  48898  mreclat  48901  rescofuf  48940