Theorem ssv 3206

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

Syntax hints:  Vcvv 2763   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  ddifss  3402  inv1  3488  unv  3489  vss  3499  disj2  3507  pwv  3839  trv  4144  xpss  4772  djussxp  4812  dmv  4883  dmresi  5002  resid  5004  ssrnres  5113  rescnvcnv  5133  cocnvcnv1  5181  relrelss  5197  dffn2  5412  oprabss  6012  ofmres  6202  f1stres  6226  f2ndres  6227  fiintim  7001  residfi  7015  djuf1olemr  7129  endjusym  7171  dju1p1e2  7278  suplocexprlemell  7799  seq3val  10571  seqvalcd  10572  seq3-1  10573  seqf  10575  seq3p1  10576  seqf2  10579  seq1cd  10580  seqp1cd  10581  seqclg  10583  seqfeq4g  10642  wrdv  10970  setscom  12745  gsumwsubmcl  13200  gsumfzcl  13203  prdsinvlem  13312  rngmgpf  13571  mgpf  13645  crngridl  14164  upxp  14616  uptx  14618  cnmptid  14625  cnmpt1st  14632  cnmpt2nd  14633