Theorem ssv 3270

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

This proof depends on syntax axioms:  Vcvv 2821   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  ddifss  3469  inv1  3559  unv  3560  vss  3568  disj2  3580  pwv  3934  trv  4241  xpss  4883  djussxp  4925  dmv  4997  dmresi  5118  resid  5120  ssrnres  5230  rescnvcnv  5250  cocnvcnv1  5298  relrelss  5314  dffn2  5535  oprabss  6174  ofmres  6369  f1stres  6393  f2ndres  6394  fiintim  7238  residfi  7254  djuf1olemr  7394  endjusym  7436  dju1p1e2  7549  suplocexprlemell  8080  seq3val  10910  seqvalcd  10911  seq3-1  10912  seqf  10914  seq3p1  10915  seqf2  10918  seq1cd  10919  seqp1cd  10920  seqclg  10922  seqfeq4g  10981  wrdv  11334  setscom  13441  gzsumwsubmcl  13850  gzsumcl  13853  prdsinvlem  14245  rngmgpf  14285  mgpf  14364  crngridl  14916  upxp  15422  uptx  15424  cnmptid  15431  cnmpt1st  15438  cnmpt2nd  15439