Theorem ssv 2077

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 1813	. 2 |- (x e. A -> x e. V)
2	1	ssriv 2065	1 |- A (_ V

Syntax hints:  Vcvv 1807   (_ wss 2043

This theorem is referenced by:  inv1 2295  unv 2296  vss 2303  pssv 2306  disj2 2312  pwv 2497  trv 2687  intabs 2728  dmv 3322  dmresi 3391  resid 3392  ssrnres 3473  cocnvcnv1 3497  fnf 3620  oprabss 3997  df1st2 4116  df2nd2 4117  fiint 4540  0vfval 8177

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049

Copyright terms: Public domain