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

Theorem ssexg 4317
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 3338 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 309 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2927 . . . 4  |-  x  e. 
_V
43ssex 4315 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2979 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 420 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2924    C_ wss 3288
This theorem is referenced by:  ssexd  4318  difexg  4319  rabexg  4321  elssabg  4323  elpw2g  4331  abssexg  4352  snexALT  4353  sess1  4518  sess2  4519  trsuc  4633  ordsssuc2  4637  unexb  4676  difex2  4681  uniexb  4719  xpexg  4956  riinint  5093  dmexg  5097  rnexg  5098  resexg  5152  resiexg  5155  imaexg  5184  exse2  5205  cnvexg  5372  coexg  5379  fabexg  5591  f1oabexg  5653  resfunexgALT  5925  cofunexg  5926  fnexALT  5929  mptexg  5932  f1dmex  5938  isofr2  6031  oprabexd  6153  ofres  6288  mpt2exxg  6389  tposexg  6460  brrpssg  6491  tz7.48-3  6668  oaabs  6854  erex  6896  mapex  6991  pmvalg  6996  elpmg  6999  pmss12g  7007  ixpexg  7053  ssdomg  7120  fiprc  7155  domunsncan  7175  infensuc  7252  pssnn  7294  unbnn  7330  fodomfi  7352  fival  7383  fiss  7395  dffi3  7402  hartogslem2  7476  card2on  7486  wdomima2g  7518  unxpwdom2  7520  unxpwdom  7521  harwdom  7522  oemapvali  7604  ackbij1lem11  8074  cofsmo  8113  ssfin4  8154  fin23lem11  8161  ssfin2  8164  ssfin3ds  8174  isfin1-3  8230  hsmex3  8278  axdc2lem  8292  ac6num  8323  zorn2lem1  8340  ttukeylem1  8353  ondomon  8402  fpwwe2lem3  8472  fpwwe2lem12  8480  fpwwe2lem13  8481  canthwe  8490  wuncss  8584  genpv  8840  genpdm  8843  hashf1lem1  11667  wrdexg  11702  wrdexb  11726  shftfval  11848  o1of2  12369  o1rlimmul  12375  isercolllem2  12422  isstruct2  13441  ressabs  13490  prdsbas  13643  fnmrc  13795  mrcfval  13796  isacs1i  13845  mreacs  13846  isssc  13983  ipolerval  14545  symgbas  15058  sylow2a  15216  islbs3  16190  istps3OLD  16950  basdif0  16981  tgval  16983  eltg  16985  eltg2  16986  tgss  16996  basgen2  17017  2basgen  17018  tgdif0  17020  bastop1  17021  resttopon  17187  restabs  17191  restcld  17198  restfpw  17205  restcls  17207  restntr  17208  ordtbas2  17217  ordtbas  17218  lmfval  17258  cnrest  17311  cmpcov  17414  cmpsublem  17424  cmpsub  17425  2ndcomap  17482  txss12  17598  ptrescn  17632  trfbas2  17836  trfbas  17837  isfildlem  17850  snfbas  17859  trfil1  17879  trfil2  17880  trufil  17903  ssufl  17911  hauspwpwf1  17980  ustval  18193  psmetres2  18306  metrest  18515  cnheibor  18941  metcld2  19220  bcthlem1  19238  mbfimaopn2  19510  0pledm  19526  dvbss  19749  dvreslem  19757  dvres2lem  19758  dvcnp2  19767  dvaddbr  19785  dvmulbr  19786  dvcnvrelem2  19863  elply2  20076  plyf  20078  plyss  20079  elplyr  20081  plyeq0lem  20090  plyeq0  20091  plyaddlem  20095  plymullem  20096  dgrlem  20109  coeidlem  20117  ulmcn  20276  pserulm  20299  iseupa  21648  issubgo  21852  rabexgfGS  23948  abrexdomjm  23949  dmct  24067  ress0g  24143  metidval  24246  indval  24372  sigagenss  24493  measval  24513  erdsze2lem1  24850  erdsze2lem2  24851  cvxpcon  24890  dfon2lem3  25363  setlikess  25417  altxpexg  25735  ivthALT  26236  islocfin  26274  filnetlem3  26307  abrexdom  26330  sdclem2  26344  sdclem1  26345  ralxpmap  26640  elrfirn  26647  elmapssres  26669  pwssplit4  27067  hbtlem1  27203  hbtlem7  27205  rabexgf  27570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator