Theorem ssv 3264

Description: Any class is a subclass of the universal class. Dual of 0ss 3551. (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 2827	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V)
2	1	ssriv 3246	1 ⊢ 𝐴 ⊆ V

Syntax hints:  Vcvv 2815   ⊆ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-v 2817  df-in 3220  df-ss 3227

This theorem is referenced by:  ddifss  3463  inv1  3549  unv  3550  vss  3557  disj2  3569  pwv  3919  trv  4226  xpss  4864  djussxp  4906  dmv  4978  dmresi  5099  resid  5101  ssrnres  5211  rescnvcnv  5231  cocnvcnv1  5279  relrelss  5295  dffn2  5516  oprabss  6148  ofmres  6343  f1stres  6367  f2ndres  6368  fiintim  7205  residfi  7221  djuf1olemr  7359  endjusym  7401  dju1p1e2  7514  suplocexprlemell  8045  seq3val  10850  seqvalcd  10851  seq3-1  10852  seqf  10854  seq3p1  10855  seqf2  10858  seq1cd  10859  seqp1cd  10860  seqclg  10862  seqfeq4g  10921  wrdv  11269  setscom  13341  gsumwsubmcl  13756  gsumfzcl  13759  prdsinvlem  14143  rngmgpf  14181  mgpf  14259  crngridl  14809  upxp  15268  uptx  15270  cnmptid  15277  cnmpt1st  15284  cnmpt2nd  15285