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

Theorem ssexg 3730
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
StepHypRef Expression
1 sseq2 2841 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 306 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2483 . . . 4  |-  x  e. 
_V
43ssex 3728 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2531 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 416 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 356    = wceq 1524    e. wcel 1526   _Vcvv 2480    C_ wss 2798
This theorem is referenced by:  difexg  3731  rabexg  3733  elssabg  3735  elpw2g  3736  abssexg  3762  snexALT  3763  sess1  3922  sess2  3923  trsuc  4037  ordsssuc2  4042  unexb  4079  difex2  4084  uniexb  4140  xpexg  4392  riinint  4527  dmexg  4531  rnexg  4532  resexg  4586  resiexg  4589  imaexg  4617  exse2  4638  soex  4713  cnvexg  4796  coexg  4803  fex2  4939  fabexg  4960  f1oabexg  5019  resfunexgALT  5197  cofunexg  5198  fnexALT  5201  mptexg  5204  f1dmex  5210  isofr2  5356  oprabexd  5465  mpt2exg  5467  ofres  5596  fnwelem  5725  fnse  5727  tposexg  5741  brrpssg  5768  tz7.48-3  5921  oaabs  6107  erex  6149  mapex  6233  pmvalg  6238  elpmg  6241  pmss12g  6249  ixpexg  6289  ssdomg  6355  f1imaen2g  6369  fiprc  6389  domunsncan  6409  infensuc  6533  pssnn  6574  unbnn  6606  fodomfi  6628  fival  6658  fiss  6669  dffi3  6676  ordtypelem10  6735  oismo  6748  hartogslem2  6751  wofib  6753  wemapso  6759  card2on  6761  wdom2d  6787  wdomd  6788  wdomima2g  6793  unxpwdom2  6795  unxpwdom  6796  harwdom  6797  cantnfle  6865  cantnflt  6866  cantnflt2  6867  cantnfp1lem2  6874  cantnfp1lem3  6875  oemapvali  6879  cantnflem1b  6881  cantnflem1d  6883  cantnflem1  6884  cnfcomlem  6895  cnfcom  6896  cnfcom2lem  6897  cnfcom3lem  6899  acni2  7165  ackbij1lem11  7329  cofsmo  7368  ssfin4  7409  fin23lem11  7416  ssfin2  7419  ssfin3ds  7429  isfin1-3  7485  fin1a2lem12  7510  hsmexlem1  7525  hsmex3  7533  axdc2lem  7547  ac6num  7574  zorn2lem1  7609  zorn2lem4  7612  ttukeylem1  7622  ondomon  7669  fpwwe2lem2  7736  fpwwe2lem3  7737  fpwwe2lem5  7738  fpwwe2lem12  7745  fpwwe2lem13  7746  fpwwe2  7747  fpwwelem  7749  canthwelem  7754  canthwe  7755  pwfseqlem4  7766  genpv  8054  genpdm  8057  hashf1lem1  10765  shftfval  10779  o1of2  11297  o1rlimmul  11303  isercolllem2  11350  hashbcss  12176  isstruct2  12281  strssd  12302  ressabs  12326  restid2  12444  prdsbas  12464  divsfval  12554  fnmrc  12612  mrcfval  12613  isacs1i  12634  mreacs  12635  ipolerval  12840  wrdexg  13045  wrdexb  13069  gass  13485  symgbas  13502  sylow2a  13660  sylow2blem2  13662  dprdres  13992  islbs3  14636  mplsubglem  14906  mpllsslem  14907  opsrtoslem2  14953  istps3OLD  15387  basdif0  15418  tgval  15420  eltg  15422  eltg2  15423  tgss  15433  basgen2  15454  2basgen  15455  tgdif0  15457  bastop1  15458  resttopon  15596  restabs  15600  restcld  15607  restfpw  15614  restcls  15615  restntr  15616  lpval  15622  ordtbaslem  15630  ordtbas2  15633  ordtbas  15634  ordtrest2  15646  lmfval  15674  cnrest  15725  cnrest2  15726  cnpresti  15728  cnprest  15729  cnprest2  15730  cmpcov  15825  cmpsublem  15835  cmpsub  15836  consuba  15855  consubclo  15859  uncon  15864  2ndcomap  15892  1stcelcls  15895  hausmapdom  15934  ptbasfi  15984  txss12  16008  ptcls  16018  ptrescn  16041  cnmpt2res  16079  qtopval2  16095  elqtop  16096  qtoprest  16116  ptuncnv  16206  ptunhmeo  16207  trfbas2  16246  trfbas  16247  isfildlem  16260  snfbas  16269  fsubbas  16270  trfil1  16289  trfil2  16290  trufil  16313  ssufl  16321  elfm  16350  rnelfmlem  16355  rnelfm  16356  fmfnfmlem4  16360  flimclslem  16387  hauspwpwf1  16390  hauspwpwdom  16391  ptcmplem1  16454  xmetres2  16633  metrest  16779  cnheibor  17156  fmcfil  17399  metcld2  17433  bcthlem1  17447  mbfimaopn2  17713  0pledm  17729  dvfval  17921  dvbss  17926  dvlmlem1  17928  dvlmlem2  17929  dvlm  17930  dvreslem  17937  dvres2lem  17938  dvcnp2  17947  dvnf  17953  dvnbss  17954  dvaddbr  17963  dvmulbr  17964  dvaddf  17967  dvmulf  17968  dvcmulf  17970  dvcof  17973  dvcnvrelem2  18031  elply2  18242  plyf  18244  plyss  18245  elplyr  18247  plyeq0lem  18256  plyeq0  18257  plyaddlem  18261  plymullem  18262  dgrlem  18275  coeidlem  18283  ulmss  18383  ulmcn  18385  pserulm  18407  issubgo  19526  erdsze2lem1  21631  erdsze2lem2  21632  cvxpcon  21670  cvmliftmolem1  21709  iseupa  21778  dfon2lem3  22032  setlikess  22088  altxpexg  22410  oprabex2gpop  22873  sndw  22937  prjmapcp  23004  prjmapcp2  23009  ubpar  23100  qusp  23387  efilcp  23397  cnfilca  23401  islimrs3  23426  islimrs4  23427  fnctartar3  23754  prismorcsetlem  23757  prismorcset  23759  lemindclsbu  23841  indcls2  23842  ivthALT  24087  islocfin  24125  neibastop2lem  24138  fnejoin1  24146  filnetlem3  24158  filnetlem4  24159  abrexdom  24235  sdclem2  24282  sdclem1  24283  ralxpmap  24593  elrfi  24601  elrfirn  24602  elrfirn2  24603  elmapssres  24624  pwssplit0  25059  pwssplit1  25060  pwssplit2  25061  pwssplit3  25062  pwssplit4  25063  frlmsplit2  25115  frlmsslss  25116  hbtlem1  25199  hbtlem7  25201  pmtrfconj  25279  bnj74  26377  bnj1412  27448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594  ax-16 1780  ax-ext 2051  ax-sep 3711
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1451  df-sb 1741  df-clab 2057  df-cleq 2062  df-clel 2065  df-v 2482  df-in 2805  df-ss 2809
  Copyright terms: Public domain W3C validator