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

Theorem ssexg 4057
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 3121 . . . 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 2730 . . . 4  |-  x  e. 
_V
43ssex 4055 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2781 . 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 6    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2727    C_ wss 3078
This theorem is referenced by:  difexg  4058  rabexg  4060  elssabg  4062  elpw2g  4063  abssexg  4089  snexALT  4090  sess1  4254  sess2  4255  trsuc  4369  ordsssuc2  4374  unexb  4411  difex2  4416  uniexb  4454  xpexg  4707  riinint  4842  dmexg  4846  rnexg  4847  resexg  4901  resiexg  4904  imaexg  4933  exse2  4954  soex  5029  cnvexg  5114  coexg  5121  fex2  5258  fabexg  5279  f1oabexg  5341  resfunexgALT  5590  cofunexg  5591  fnexALT  5594  mptexg  5597  f1dmex  5603  isofr2  5693  oprabexd  5812  ofres  5946  mpt2exxg  6047  fnwelem  6082  fnse  6084  tposexg  6100  brrpssg  6131  tz7.48-3  6342  oaabs  6528  erex  6570  mapex  6664  pmvalg  6669  elpmg  6672  pmss12g  6680  ixpexg  6726  ssdomg  6793  f1imaen2g  6807  fiprc  6827  domunsncan  6847  infensuc  6924  pssnn  6966  unbnn  6998  fodomfi  7020  fival  7050  fiss  7061  dffi3  7068  ordtypelem10  7126  oismo  7139  hartogslem2  7142  wofib  7144  wemapso  7150  card2on  7152  wdom2d  7178  wdomd  7179  wdomima2g  7184  unxpwdom2  7186  unxpwdom  7187  harwdom  7188  cantnfle  7256  cantnflt  7257  cantnflt2  7258  cantnfp1lem2  7265  cantnfp1lem3  7266  oemapvali  7270  cantnflem1b  7272  cantnflem1d  7274  cantnflem1  7275  cnfcomlem  7286  cnfcom  7287  cnfcom2lem  7288  cnfcom3lem  7290  acni2  7557  ackbij1lem11  7740  cofsmo  7779  ssfin4  7820  fin23lem11  7827  ssfin2  7830  ssfin3ds  7840  isfin1-3  7896  fin1a2lem12  7921  hsmexlem1  7936  hsmex3  7944  axdc2lem  7958  ac6num  7990  zorn2lem1  8007  zorn2lem4  8010  ttukeylem1  8020  ondomon  8067  fpwwe2lem2  8134  fpwwe2lem3  8135  fpwwe2lem5  8136  fpwwe2lem12  8143  fpwwe2lem13  8144  fpwwe2  8145  fpwwelem  8147  canthwelem  8152  canthwe  8153  pwfseqlem4  8164  wuncss  8247  genpv  8503  genpdm  8506  hashf1lem1  11270  wrdexg  11302  wrdexb  11326  shftfval  11442  o1of2  11963  o1rlimmul  11969  isercolllem2  12016  hashbcss  12925  isstruct2  13031  strssd  13056  ressabs  13080  restid2  13209  prdsbas  13231  divsfval  13323  fnmrc  13381  mrcfval  13382  isacs1i  13403  mreacs  13404  isssc  13541  rescabs  13554  rescabs2  13555  resssetc  13768  resscatc  13781  yonedalem1  13890  yonedalem21  13891  yonedalem3a  13892  yonedalem4c  13895  yonedalem22  13896  yonedalem3b  13897  yonedainv  13899  yonffthlem  13900  ipolerval  14103  gass  14590  symgbas  14607  sylow2a  14765  sylow2blem2  14767  dprdres  15098  islbs3  15742  mplsubglem  16011  mpllsslem  16012  opsrtoslem2  16058  istps3OLD  16492  basdif0  16523  tgval  16525  eltg  16527  eltg2  16528  tgss  16538  basgen2  16559  2basgen  16560  tgdif0  16562  bastop1  16563  lpval  16703  resttopon  16724  restabs  16728  restcld  16735  restfpw  16742  restcls  16743  restntr  16744  ordtbaslem  16750  ordtbas2  16753  ordtbas  16754  ordtrest2  16766  lmfval  16794  cnrest  16845  cnrest2  16846  cnpresti  16848  cnprest  16849  cnprest2  16850  cmpcov  16948  cmpsublem  16958  cmpsub  16959  consuba  16978  consubclo  16982  uncon  16987  2ndcomap  17016  1stcelcls  17019  hausmapdom  17058  ptbasfi  17108  txss12  17132  ptcls  17142  ptrescn  17165  cnmpt2res  17203  qtopval2  17219  elqtop  17220  qtoprest  17240  ptuncnv  17330  ptunhmeo  17331  trfbas2  17370  trfbas  17371  isfildlem  17384  snfbas  17393  fsubbas  17394  trfil1  17413  trfil2  17414  trufil  17437  ssufl  17445  elfm  17474  rnelfmlem  17479  rnelfm  17480  fmfnfmlem4  17484  flimclslem  17511  hauspwpwf1  17514  hauspwpwdom  17515  ptcmplem1  17578  xmetres2  17757  metrest  17902  cnheibor  18285  fmcfil  18530  metcld2  18564  bcthlem1  18578  mbfimaopn2  18844  0pledm  18860  dvbss  19083  dvreslem  19091  dvres2lem  19092  dvcnp2  19101  dvnf  19108  dvnbss  19109  dvaddbr  19119  dvmulbr  19120  dvaddf  19123  dvmulf  19124  dvcmulf  19126  dvcof  19129  dvcnvrelem2  19197  elply2  19410  plyf  19412  plyss  19413  elplyr  19415  plyeq0lem  19424  plyeq0  19425  plyaddlem  19429  plymullem  19430  dgrlem  19443  coeidlem  19451  ulmss  19606  ulmcn  19608  pserulm  19630  issubgo  20800  erdsze2lem1  22905  erdsze2lem2  22906  cvxpcon  22944  cvmliftmolem1  22983  iseupa  23052  dfon2lem3  23309  setlikess  23363  altxpexg  23686  oprabex2gpop  24201  sndw  24265  prjmapcp  24331  prjmapcp2  24336  ubpar  24427  qusp  24708  efilcp  24718  cnfilca  24722  islimrs3  24747  islimrs4  24748  fnctartar3  25075  prismorcsetlem  25078  prismorcset  25080  lemindclsbu  25161  indcls2  25162  ivthALT  25424  islocfin  25462  neibastop2lem  25475  fnejoin1  25483  filnetlem3  25495  filnetlem4  25496  abrexdom  25571  sdclem2  25618  sdclem1  25619  ralxpmap  25927  elrfi  25935  elrfirn  25936  elrfirn2  25937  elmapssres  25958  pwssplit0  26353  pwssplit1  26354  pwssplit2  26355  pwssplit3  26356  pwssplit4  26357  frlmsplit2  26409  frlmsslss  26410  hbtlem1  26493  hbtlem7  26495  pmtrfconj  26573  bnj1413  27754
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 1926  ax-ext 2234  ax-sep 4038
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator