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

Theorem ssexg 4126
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.)
Assertion
Ref Expression
ssexg  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )

Proof of Theorem ssexg
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sseq2 3171 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 230 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2733 . . . 4  |-  x  e. 
_V
43ssex 4124 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2790 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 124 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1348    e. wcel 2141   _Vcvv 2730    C_ wss 3121
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-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4105
This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134
This theorem is referenced by:  ssexd  4127  difexg  4128  rabexg  4130  elssabg  4132  elpw2g  4140  abssexg  4166  snexg  4168  sess1  4320  sess2  4321  trsuc  4405  unexb  4425  abnexg  4429  uniexb  4456  xpexg  4723  riinint  4870  dmexg  4873  rnexg  4874  resexg  4929  resiexg  4934  imaexg  4963  exse2  4983  cnvexg  5146  coexg  5153  fabexg  5383  f1oabexg  5452  relrnfvex  5512  fvexg  5513  sefvex  5515  mptfvex  5579  mptexg  5718  ofres  6072  resfunexgALT  6084  cofunexg  6085  fnexALT  6087  f1dmex  6092  oprabexd  6103  mpoexxg  6186  tposexg  6234  frecabex  6374  erex  6533  mapex  6628  pmvalg  6633  elpmg  6638  elmapssres  6647  pmss12g  6649  ixpexgg  6696  ssdomg  6752  fiprc  6789  fival  6943  iccen  9950  shftfvalg  10769  shftfval  10772  toponsspwpwg  12773  tgval  12802  tgvalex  12803  eltg  12805  eltg2  12806  tgss  12816  basgen2  12834  bastop1  12836  topnex  12839  resttopon  12924  restabs  12928  lmfval  12945  cnrest  12988  txss12  13019  metrest  13259  dvbss  13407  dvcnp2cntop  13416  dvaddxxbr  13418  dvmulxxbr  13419
  Copyright terms: Public domain W3C validator