Theorem ssv 3250

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

Syntax hints:  Vcvv 2803   ⊆ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805  df-in 3207  df-ss 3214

This theorem is referenced by:  ddifss  3447  inv1  3533  unv  3534  vss  3544  disj2  3552  pwv  3897  trv  4204  xpss  4840  djussxp  4881  dmv  4953  dmresi  5074  resid  5076  ssrnres  5186  rescnvcnv  5206  cocnvcnv1  5254  relrelss  5270  dffn2  5491  oprabss  6117  ofmres  6307  f1stres  6331  f2ndres  6332  fiintim  7166  residfi  7182  djuf1olemr  7296  endjusym  7338  dju1p1e2  7451  suplocexprlemell  7976  seq3val  10768  seqvalcd  10769  seq3-1  10770  seqf  10772  seq3p1  10773  seqf2  10776  seq1cd  10777  seqp1cd  10778  seqclg  10780  seqfeq4g  10839  wrdv  11178  setscom  13185  gsumwsubmcl  13642  gsumfzcl  13645  prdsinvlem  13754  rngmgpf  14014  mgpf  14088  crngridl  14609  upxp  15066  uptx  15068  cnmptid  15075  cnmpt1st  15082  cnmpt2nd  15083