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

Theorem ssex 4581
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 4558 (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 3475 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 ssex.1 . . . 4  |-  B  e. 
_V
32inex2 4579 . . 3  |-  ( A  i^i  B )  e. 
_V
4 eleq1 2515 . . 3  |-  ( ( A  i^i  B )  =  A  ->  (
( A  i^i  B
)  e.  _V  <->  A  e.  _V ) )
53, 4mpbii 211 . 2  |-  ( ( A  i^i  B )  =  A  ->  A  e.  _V )
61, 5sylbi 195 1  |-  ( A 
C_  B  ->  A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   _Vcvv 3095    i^i cin 3460    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475
This theorem is referenced by:  ssexi  4582  ssexg  4583  intex  4593  moabex  4696  ixpiunwdom  8020  omex  8063  tcss  8178  bndrank  8262  scottex  8306  aceq3lem  8504  cfslb  8649  dcomex  8830  axdc2lem  8831  grothpw  9207  grothpwex  9208  grothomex  9210  elnp  9368  hashfacen  12485  limsuple  13283  limsuplt  13284  limsupbnd1  13287  o1add2  13428  o1mul2  13429  o1sub2  13430  o1dif  13434  caucvgrlem  13477  fsumo1  13608  unbenlem  14408  ressbas2  14670  prdsval  14834  prdsbas  14836  rescbas  15180  reschom  15181  rescco  15183  acsmapd  15787  issubmnd  15927  eqgfval  16228  dfod2  16565  ablfac1b  17100  islinds2  18826  pmatcollpw3lem  19262  2basgen  19470  prdstopn  20107  ressust  20745  rectbntr0  21315  elcncf  21371  cncfcnvcn  21403  cmsss  21767  ovolctb2  21881  limcfval  22254  ellimc2  22259  limcflf  22263  limcres  22268  limcun  22277  dvfval  22279  lhop2  22394  taylfval  22732  ulmval  22753  xrlimcnp  23276  axtgcont1  23843  fpwrelmap  27534  ressnm  27617  ressprs  27621  ordtrestNEW  27881  ddeval1  28184  ddeval0  28185  msrval  28876  mclsval  28901  brsset  29515  mblfinlem3  30029  isfne4  30134  refssfne  30152  topjoin  30159  filbcmb  30207  cnpwstotbnd  30269  ismtyval  30272  isnumbasgrplem2  31029  mulcncff  31624  subcncff  31636  addcncff  31641  cncfuni  31643  divcncff  31648  etransclem1  31972  etransclem4  31975  etransclem13  31984  issubmgm2  32432  linccl  32885  ellcoellss  32906  bnj849  33851  bj-snglex  34414  ispsubsp  35344  ispsubclN  35536
  Copyright terms: Public domain W3C validator