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

Theorem ssexg 3953
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 3037 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 229 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2618 . . . 4  |-  x  e. 
_V
43ssex 3951 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2672 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 123 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1287    e. wcel 1436   _Vcvv 2615    C_ wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3932
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994  df-ss 3001
This theorem is referenced by:  ssexd  3954  difexg  3955  rabexg  3957  elssabg  3959  elpw2g  3967  abssexg  3991  snexg  3993  sess1  4138  sess2  4139  trsuc  4223  unexb  4241  uniexb  4269  xpexg  4520  riinint  4662  dmexg  4665  rnexg  4666  resexg  4719  resiexg  4724  imaexg  4753  exse2  4773  cnvexg  4934  coexg  4941  fabexg  5161  f1oabexg  5228  relrnfvex  5286  fvexg  5287  sefvex  5289  mptfvex  5351  mptexg  5483  ofres  5826  resfunexgALT  5838  cofunexg  5839  fnexALT  5841  f1dmex  5844  oprabexd  5855  mpt2exxg  5934  tposexg  5977  frecabex  6117  erex  6268  mapex  6363  pmvalg  6368  elpmg  6373  elmapssres  6382  pmss12g  6384  ssdomg  6447  fiprc  6484  shftfvalg  10149  shftfval  10152
  Copyright terms: Public domain W3C validator