Theorem ssv 3191

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

Syntax hints:  Vcvv 2751   ⊆ wss 3143

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-v 2753  df-in 3149  df-ss 3156

This theorem is referenced by:  ddifss  3387  inv1  3473  unv  3474  vss  3484  disj2  3492  pwv  3822  trv  4127  xpss  4748  djussxp  4786  dmv  4857  dmresi  4976  resid  4978  ssrnres  5085  rescnvcnv  5105  cocnvcnv1  5153  relrelss  5169  dffn2  5381  oprabss  5976  ofmres  6154  f1stres  6177  f2ndres  6178  fiintim  6945  djuf1olemr  7070  endjusym  7112  dju1p1e2  7213  suplocexprlemell  7729  seq3val  10475  seqvalcd  10476  seq3-1  10477  seqf  10478  seq3p1  10479  seqf2  10481  seq1cd  10482  seqp1cd  10483  setscom  12519  rngmgpf  13251  mgpf  13325  crngridl  13804  upxp  14155  uptx  14157  cnmptid  14164  cnmpt1st  14171  cnmpt2nd  14172