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

Theorem ssexg 3924
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 2995 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 224 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2577 . . . 4  |-  x  e. 
_V
43ssex 3922 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2630 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 120 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    = wceq 1259    e. wcel 1409   _Vcvv 2574    C_ wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952  df-ss 2959
This theorem is referenced by:  ssexd  3925  difexg  3926  rabexg  3928  elssabg  3930  elpw2g  3938  abssexg  3962  snexgOLD  3963  snexg  3964  sess1  4102  sess2  4103  trsuc  4187  unexb  4205  uniexb  4233  xpexg  4480  riinint  4621  dmexg  4624  rnexg  4625  resexg  4678  resiexg  4681  imaexg  4708  exse2  4727  cnvexg  4883  coexg  4890  fabexg  5105  f1oabexg  5166  relrnfvex  5221  fvexg  5222  sefvex  5224  mptfvex  5284  mptexg  5414  ofres  5753  resfunexgALT  5765  cofunexg  5766  fnexALT  5768  f1dmex  5771  oprabexd  5782  mpt2exxg  5861  tposexg  5904  frecabex  6015  erex  6161  ssdomg  6289  fiprc  6323  shftfvalg  9647  shftfval  9650
  Copyright terms: Public domain W3C validator