Theorem ssv 3971

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

Syntax hints:  Vcvv 3447   ⊆ wss 3914

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931

This theorem is referenced by:  inv1  4361  unv  4362  vss  4409  pssv  4412  disj2  4421  pwv  4868  unissint  4936  symdifv  5050  trv  5228  intabs  5304  xpss  5654  inxpssres  5655  djussxp  5809  dmv  5886  dmresi  6023  cnvrescnv  6168  rescnvcnv  6177  cocnvcnv1  6230  relrelss  6246  fnresi  6647  dffn2  6690  oprabss  7497  fvresex  7938  ofmres  7963  f1stres  7992  f2ndres  7993  fsplitfpar  8097  domssex2  9101  fineqv  9210  fiint  9277  fiintOLD  9278  marypha1lem  9384  marypha2  9390  cantnfval2  9622  cottrcl  9672  inlresf1  9868  inrresf1  9870  djuun  9879  dfac12lem2  10098  dfac12a  10102  fin23lem41  10305  dfacfin7  10352  iunfo  10492  gch2  10628  axpre-sup  11122  wrdv  14494  setscom  17150  isofn  17737  homaf  17992  dmaf  18011  cdaf  18012  prdsinvlem  18981  frgpuplem  19702  gsum2dlem2  19901  gsum2d  19902  prdsmgp  20060  rngmgpf  20066  mgpf  20157  prdscrngd  20231  pws1  20234  mulgass3  20262  crngridl  21190  frlmbas  21664  islindf3  21735  psdmul  22053  ply1lss  22081  coe1fval3  22093  coe1tm  22159  ply1coe  22185  evl1expd  22232  pmatcollpw3lem  22670  clsconn  23317  ptbasfi  23468  upxp  23510  uptx  23512  prdstps  23516  hausdiag  23532  cnmpt1st  23555  cnmpt2nd  23556  fbssint  23725  prdstmdd  24011  prdsxmslem2  24417  isngp2  24485  uniiccdif  25479  wlkdlem1  29610  0vfval  30535  xppreima  32569  2ndimaxp  32570  2ndresdju  32573  xppreima2  32575  1stpreimas  32629  fsuppcurry1  32648  fsuppcurry2  32649  ffsrn  32652  gsummpt2d  32989  gsumpart  32997  elrgspnlem2  33194  lindflbs  33350  elrspunidl  33399  dimval  33596  dimvalfi  33597  qtophaus  33826  cnre2csqlem  33900  cntmeas  34216  eulerpartlemmf  34366  eulerpartlemgf  34370  sseqfv1  34380  sseqfn  34381  sseqfv2  34385  coinflippv  34475  fineqvacALT  35088  gblacfnacd  35089  vonf1owev  35095  wevgblacfn  35096  erdszelem2  35179  mpstssv  35526  filnetlem4  36369  bj-0int  37089  bj-idres  37148  elxp8  37359  poimirlem26  37640  poimirlem27  37641  heibor1lem  37803  rmxyelqirrOLD  42899  isnumbasgrplem1  43090  isnumbasgrplem2  43093  dfacbasgrp  43097  resnonrel  43581  comptiunov2i  43695  ntrneiel2  44075  ntrneik4w  44089  conss2  44432  permaxun  45001  permac8prim  45004  slotresfo  48887  basresposfo  48966  ipoglb0  48982  mreclat  48985  isofnALT  49020  rescofuf  49082  initopropdlem  49229  termopropdlem  49230  zeroopropdlem  49231