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

Theorem ssv 3089
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 2671 . 2 (𝑥𝐴𝑥 ∈ V)
21ssriv 3071 1 𝐴 ⊆ V
Colors of variables: wff set class
Syntax hints:  Vcvv 2660  wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662  df-in 3047  df-ss 3054
This theorem is referenced by:  ddifss  3284  inv1  3369  unv  3370  vss  3380  disj2  3388  pwv  3705  trv  4008  xpss  4617  djussxp  4654  dmv  4725  dmresi  4844  resid  4845  ssrnres  4951  rescnvcnv  4971  cocnvcnv1  5019  relrelss  5035  dffn2  5244  oprabss  5825  ofmres  6002  f1stres  6025  f2ndres  6026  fiintim  6785  djuf1olemr  6907  endjusym  6949  dju1p1e2  7021  suplocexprlemell  7489  seq3val  10199  seqvalcd  10200  seq3-1  10201  seqf  10202  seq3p1  10203  seqf2  10205  seq1cd  10206  seqp1cd  10207  setscom  11926  upxp  12368  uptx  12370  cnmptid  12377  cnmpt1st  12384  cnmpt2nd  12385
  Copyright terms: Public domain W3C validator