Theorem ssv 3169

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

Syntax hints:  Vcvv 2730   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  ddifss  3365  inv1  3451  unv  3452  vss  3462  disj2  3470  pwv  3795  trv  4099  xpss  4719  djussxp  4756  dmv  4827  dmresi  4946  resid  4947  ssrnres  5053  rescnvcnv  5073  cocnvcnv1  5121  relrelss  5137  dffn2  5349  oprabss  5939  ofmres  6115  f1stres  6138  f2ndres  6139  fiintim  6906  djuf1olemr  7031  endjusym  7073  dju1p1e2  7174  suplocexprlemell  7675  seq3val  10414  seqvalcd  10415  seq3-1  10416  seqf  10417  seq3p1  10418  seqf2  10420  seq1cd  10421  seqp1cd  10422  setscom  12456  upxp  13066  uptx  13068  cnmptid  13075  cnmpt1st  13082  cnmpt2nd  13083