Theorem ssv 2081

Description: Any class is a subclass of the universal class.

Assertion

Ref	Expression
ssv	|- A (_ V

Proof of Theorem ssv

Step	Hyp	Ref	Expression
1		elisset 1817	. 2 |- (x e. A -> x e. V)
2	1	ssriv 2069	1 |- A (_ V

Syntax hints:  Vcvv 1811   (_ wss 2047

This theorem is referenced by:  inv1 2299  unv 2300  vss 2307  pssv 2310  disj2 2316  pwv 2502  trv 2692  intabs 2733  dmv 3327  dmresi 3399  resid 3400  ssrnres 3481  cocnvcnv1 3505  fnf 3628  oprabss 4006  df1st2 4126  df2nd2 4127  fiint 4559  fiintOLD 4560  0vfval 8225

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053

Copyright terms: Public domain