MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssex Unicode version

Theorem ssex 4098
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4081 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
ssex.1  |-  B  e. 
_V
Assertion
Ref Expression
ssex  |-  ( A 
C_  B  ->  A  e.  _V )

Proof of Theorem ssex
StepHypRef Expression
1 df-ss 3108 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4096 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2316 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 204 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 189 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619    e. wcel 1621   _Vcvv 2740    i^i cin 3093    C_ wss 3094
This theorem is referenced by:  ssexi  4099  ssexg  4100  intex  4109  moabex  4170  ixpiunwdom  7238  omex  7277  tcss  7362  bndrank  7446  scottex  7488  aceq3lem  7680  cfslb  7825  dcomex  8006  axdc2lem  8007  grothpw  8381  grothpwex  8382  grothomex  8384  elnp  8544  hashfacen  11322  limsuple  11882  limsuplt  11883  limsupbnd1  11886  o1add2  12027  o1mul2  12028  o1sub2  12029  o1dif  12033  caucvgrlem  12075  fsumo1  12200  unbenlem  12882  ressbas2  13126  prdsval  13282  prdsbas  13284  rescbas  13633  reschom  13634  rescco  13636  acsmapd  14208  issubmnd  14328  eqgfval  14592  dfod2  14804  ablfac1b  15232  2basgen  16655  prdstopn  17249  rectbntr0  18264  elcncf  18320  cncfcnvcn  18351  cmsss  18699  ovolctb2  18778  limcfval  19149  ellimc2  19154  limcflf  19158  limcres  19163  limcun  19172  dvfval  19174  lhop2  19289  taylfval  19665  ulmval  19686  xrlimcnp  20190  ballotlemelo  22972  brsset  23770  supnuf  24961  supexr  24963  vtarsuelt  25227  isfne4  25601  refssfne  25626  topjoin  25646  filbcmb  25764  cnpwstotbnd  25853  ismtyval  25856  isnumbasgrplem2  26601  islinds2  26615  bnj849  27969  ispsubsp  29064  ispsubclN  29256
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator