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

Theorem ssexg 4351
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 3372 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 310 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2961 . . . 4  |-  x  e. 
_V
43ssex 4349 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 3013 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 421 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958    C_ wss 3322
This theorem is referenced by:  ssexd  4352  difexg  4353  rabexg  4355  elssabg  4357  elpw2g  4365  abssexg  4386  snexALT  4387  sess1  4552  sess2  4553  trsuc  4668  ordsssuc2  4672  unexb  4711  difex2  4716  uniexb  4754  xpexg  4991  riinint  5128  dmexg  5132  rnexg  5133  resexg  5187  resiexg  5190  imaexg  5219  exse2  5240  cnvexg  5407  coexg  5414  fabexg  5626  f1oabexg  5688  resfunexgALT  5960  cofunexg  5961  fnexALT  5964  mptexg  5967  f1dmex  5973  isofr2  6066  oprabexd  6188  ofres  6323  mpt2exxg  6424  tposexg  6495  brrpssg  6526  tz7.48-3  6703  oaabs  6889  erex  6931  mapex  7026  pmvalg  7031  elpmg  7034  pmss12g  7042  ixpexg  7088  ssdomg  7155  fiprc  7190  domunsncan  7210  infensuc  7287  pssnn  7329  unbnn  7365  fodomfi  7387  fival  7419  fiss  7431  dffi3  7438  hartogslem2  7514  card2on  7524  wdomima2g  7556  unxpwdom2  7558  unxpwdom  7559  harwdom  7560  oemapvali  7642  ackbij1lem11  8112  cofsmo  8151  ssfin4  8192  fin23lem11  8199  ssfin2  8202  ssfin3ds  8212  isfin1-3  8268  hsmex3  8316  axdc2lem  8330  ac6num  8361  zorn2lem1  8378  ttukeylem1  8391  ondomon  8440  fpwwe2lem3  8510  fpwwe2lem12  8518  fpwwe2lem13  8519  canthwe  8528  wuncss  8622  genpv  8878  genpdm  8881  hashf1lem1  11706  wrdexg  11741  wrdexb  11765  shftfval  11887  o1of2  12408  o1rlimmul  12414  isercolllem2  12461  isstruct2  13480  ressabs  13529  prdsbas  13682  fnmrc  13834  mrcfval  13835  isacs1i  13884  mreacs  13885  isssc  14022  ipolerval  14584  symgbas  15097  sylow2a  15255  islbs3  16229  istps3OLD  16989  basdif0  17020  tgval  17022  eltg  17024  eltg2  17025  tgss  17035  basgen2  17056  2basgen  17057  tgdif0  17059  bastop1  17060  resttopon  17227  restabs  17231  restcld  17238  restfpw  17245  restcls  17247  restntr  17248  ordtbas2  17257  ordtbas  17258  lmfval  17298  cnrest  17351  cmpcov  17454  cmpsublem  17464  cmpsub  17465  2ndcomap  17523  txss12  17639  ptrescn  17673  trfbas2  17877  trfbas  17878  isfildlem  17891  snfbas  17900  trfil1  17920  trfil2  17921  trufil  17944  ssufl  17952  hauspwpwf1  18021  ustval  18234  psmetres2  18347  metrest  18556  cnheibor  18982  metcld2  19261  bcthlem1  19279  mbfimaopn2  19551  0pledm  19567  dvbss  19790  dvreslem  19798  dvres2lem  19799  dvcnp2  19808  dvaddbr  19826  dvmulbr  19827  dvcnvrelem2  19904  elply2  20117  plyf  20119  plyss  20120  elplyr  20122  plyeq0lem  20131  plyeq0  20132  plyaddlem  20136  plymullem  20137  dgrlem  20150  coeidlem  20158  ulmcn  20317  pserulm  20340  iseupa  21689  issubgo  21893  rabexgfGS  23989  abrexdomjm  23990  dmct  24108  ress0g  24184  metidval  24287  indval  24413  sigagenss  24534  measval  24554  erdsze2lem1  24891  erdsze2lem2  24892  cvxpcon  24931  dfon2lem3  25414  setlikess  25472  altxpexg  25825  ivthALT  26340  islocfin  26378  filnetlem3  26411  abrexdom  26434  sdclem2  26448  sdclem1  26449  ralxpmap  26744  elrfirn  26751  elmapssres  26773  pwssplit4  27170  hbtlem1  27306  hbtlem7  27308  rabexgf  27673  hashss  28180
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator