Theorem ssv 3247

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

Syntax hints:  Vcvv 2800   ⊆ wss 3198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-v 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  ddifss  3443  inv1  3529  unv  3530  vss  3540  disj2  3548  pwv  3890  trv  4197  xpss  4832  djussxp  4873  dmv  4945  dmresi  5066  resid  5068  ssrnres  5177  rescnvcnv  5197  cocnvcnv1  5245  relrelss  5261  dffn2  5481  oprabss  6102  ofmres  6293  f1stres  6317  f2ndres  6318  fiintim  7116  residfi  7130  djuf1olemr  7244  endjusym  7286  dju1p1e2  7398  suplocexprlemell  7923  seq3val  10712  seqvalcd  10713  seq3-1  10714  seqf  10716  seq3p1  10717  seqf2  10720  seq1cd  10721  seqp1cd  10722  seqclg  10724  seqfeq4g  10783  wrdv  11119  setscom  13112  gsumwsubmcl  13569  gsumfzcl  13572  prdsinvlem  13681  rngmgpf  13940  mgpf  14014  crngridl  14534  upxp  14986  uptx  14988  cnmptid  14995  cnmpt1st  15002  cnmpt2nd  15003