ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssv GIF version

Theorem ssv 3087
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.
StepHypRef Expression
1 elex 2669 . 2 (𝑥𝐴𝑥 ∈ V)
21ssriv 3069 1 𝐴 ⊆ V
Colors of variables: wff set class
Syntax hints:  Vcvv 2658  wss 3039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2660  df-in 3045  df-ss 3052
This theorem is referenced by:  ddifss  3282  inv1  3367  unv  3368  vss  3378  disj2  3386  pwv  3703  trv  4006  xpss  4615  djussxp  4652  dmv  4723  dmresi  4842  resid  4843  ssrnres  4949  rescnvcnv  4969  cocnvcnv1  5017  relrelss  5033  dffn2  5242  oprabss  5823  ofmres  6000  f1stres  6023  f2ndres  6024  fiintim  6783  djuf1olemr  6905  endjusym  6947  dju1p1e2  7017  suplocexprlemell  7485  seq3val  10182  seqvalcd  10183  seq3-1  10184  seqf  10185  seq3p1  10186  seqf2  10188  seq1cd  10189  seqp1cd  10190  setscom  11905  upxp  12347  uptx  12349  cnmptid  12356  cnmpt1st  12363  cnmpt2nd  12364
  Copyright terms: Public domain W3C validator