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

Theorem ssexg 4036
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 3101 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 307 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2715 . . . 4  |-  x  e. 
_V
43ssex 4034 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2766 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 417 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 5    /\ wa 357    = wceq 1608    e. wcel 1610   _Vcvv 2712    C_ wss 3058
This theorem is referenced by:  difexg  4037  rabexg  4039  elssabg  4041  elpw2g  4042  abssexg  4068  snexALT  4069  sess1  4233  sess2  4234  trsuc  4348  ordsssuc2  4353  unexb  4390  difex2  4395  uniexb  4433  xpexg  4686  riinint  4821  dmexg  4825  rnexg  4826  resexg  4880  resiexg  4883  imaexg  4912  exse2  4933  soex  5008  cnvexg  5093  coexg  5100  fex2  5236  fabexg  5257  f1oabexg  5316  resfunexgALT  5565  cofunexg  5566  fnexALT  5569  mptexg  5572  f1dmex  5578  isofr2  5668  oprabexd  5786  ofres  5920  mpt2exxg  6021  fnwelem  6056  fnse  6058  tposexg  6074  brrpssg  6105  tz7.48-3  6316  oaabs  6502  erex  6544  mapex  6638  pmvalg  6643  elpmg  6646  pmss12g  6654  ixpexg  6700  ssdomg  6767  f1imaen2g  6781  fiprc  6801  domunsncan  6821  infensuc  6898  pssnn  6940  unbnn  6972  fodomfi  6994  fival  7024  fiss  7035  dffi3  7042  ordtypelem10  7100  oismo  7113  hartogslem2  7116  wofib  7118  wemapso  7124  card2on  7126  wdom2d  7152  wdomd  7153  wdomima2g  7158  unxpwdom2  7160  unxpwdom  7161  harwdom  7162  cantnfle  7230  cantnflt  7231  cantnflt2  7232  cantnfp1lem2  7239  cantnfp1lem3  7240  oemapvali  7244  cantnflem1b  7246  cantnflem1d  7248  cantnflem1  7249  cnfcomlem  7260  cnfcom  7261  cnfcom2lem  7262  cnfcom3lem  7264  acni2  7531  ackbij1lem11  7714  cofsmo  7753  ssfin4  7794  fin23lem11  7801  ssfin2  7804  ssfin3ds  7814  isfin1-3  7870  fin1a2lem12  7895  hsmexlem1  7910  hsmex3  7918  axdc2lem  7932  ac6num  7964  zorn2lem1  7981  zorn2lem4  7984  ttukeylem1  7994  ondomon  8041  fpwwe2lem2  8108  fpwwe2lem3  8109  fpwwe2lem5  8110  fpwwe2lem12  8117  fpwwe2lem13  8118  fpwwe2  8119  fpwwelem  8121  canthwelem  8126  canthwe  8127  pwfseqlem4  8138  wuncss  8221  genpv  8477  genpdm  8480  hashf1lem1  11206  wrdexg  11238  wrdexb  11262  shftfval  11378  o1of2  11897  o1rlimmul  11903  isercolllem2  11950  hashbcss  12859  isstruct2  12965  strssd  12990  ressabs  13014  restid2  13143  prdsbas  13165  divsfval  13257  fnmrc  13315  mrcfval  13316  isacs1i  13337  mreacs  13338  isssc  13469  rescabs  13482  rescabs2  13483  resssetc  13645  resscatc  13657  ipolerval  13949  gass  14436  symgbas  14453  sylow2a  14611  sylow2blem2  14613  dprdres  14944  islbs3  15588  mplsubglem  15857  mpllsslem  15858  opsrtoslem2  15904  istps3OLD  16338  basdif0  16369  tgval  16371  eltg  16373  eltg2  16374  tgss  16384  basgen2  16405  2basgen  16406  tgdif0  16408  bastop1  16409  lpval  16549  resttopon  16570  restabs  16574  restcld  16581  restfpw  16588  restcls  16589  restntr  16590  ordtbaslem  16596  ordtbas2  16599  ordtbas  16600  ordtrest2  16612  lmfval  16640  cnrest  16691  cnrest2  16692  cnpresti  16694  cnprest  16695  cnprest2  16696  cmpcov  16794  cmpsublem  16804  cmpsub  16805  consuba  16824  consubclo  16828  uncon  16833  2ndcomap  16862  1stcelcls  16865  hausmapdom  16904  ptbasfi  16954  txss12  16978  ptcls  16988  ptrescn  17011  cnmpt2res  17049  qtopval2  17065  elqtop  17066  qtoprest  17086  ptuncnv  17176  ptunhmeo  17177  trfbas2  17216  trfbas  17217  isfildlem  17230  snfbas  17239  fsubbas  17240  trfil1  17259  trfil2  17260  trufil  17283  ssufl  17291  elfm  17320  rnelfmlem  17325  rnelfm  17326  fmfnfmlem4  17330  flimclslem  17357  hauspwpwf1  17360  hauspwpwdom  17361  ptcmplem1  17424  xmetres2  17603  metrest  17748  cnheibor  18131  fmcfil  18376  metcld2  18410  bcthlem1  18424  mbfimaopn2  18690  0pledm  18706  dvbss  18929  dvreslem  18937  dvres2lem  18938  dvcnp2  18947  dvnf  18954  dvnbss  18955  dvaddbr  18965  dvmulbr  18966  dvaddf  18969  dvmulf  18970  dvcmulf  18972  dvcof  18975  dvcnvrelem2  19043  elply2  19256  plyf  19258  plyss  19259  elplyr  19261  plyeq0lem  19270  plyeq0  19271  plyaddlem  19275  plymullem  19276  dgrlem  19289  coeidlem  19297  ulmss  19452  ulmcn  19454  pserulm  19476  issubgo  20601  erdsze2lem1  22706  erdsze2lem2  22707  cvxpcon  22745  cvmliftmolem1  22784  iseupa  22853  dfon2lem3  23115  setlikess  23169  altxpexg  23492  oprabex2gpop  24007  sndw  24071  prjmapcp  24137  prjmapcp2  24142  ubpar  24233  qusp  24514  efilcp  24524  cnfilca  24528  islimrs3  24553  islimrs4  24554  fnctartar3  24881  prismorcsetlem  24884  prismorcset  24886  lemindclsbu  24967  indcls2  24968  ivthALT  25230  islocfin  25268  neibastop2lem  25281  fnejoin1  25289  filnetlem3  25301  filnetlem4  25302  abrexdom  25377  sdclem2  25424  sdclem1  25425  ralxpmap  25733  elrfi  25741  elrfirn  25742  elrfirn2  25743  elmapssres  25764  pwssplit0  26159  pwssplit1  26160  pwssplit2  26161  pwssplit3  26162  pwssplit4  26163  frlmsplit2  26215  frlmsslss  26216  hbtlem1  26299  hbtlem7  26301  pmtrfconj  26379  bnj1413  27501
This theorem was proved from axioms:  ax-1 6  ax-2 7  ax-3 8  ax-mp 9  ax-5 1522  ax-6 1523  ax-7 1524  ax-gen 1525  ax-8 1612  ax-11 1613  ax-17 1617  ax-12o 1653  ax-10 1667  ax-9 1673  ax-4 1681  ax-16 1915  ax-ext 2222  ax-sep 4017
This theorem depends on definitions:  df-bi 176  df-or 358  df-an 359  df-tru 1309  df-ex 1527  df-nf 1529  df-sb 1872  df-clab 2228  df-cleq 2234  df-clel 2237  df-nfc 2362  df-v 2714  df-in 3065  df-ss 3069
  Copyright terms: Public domain W3C validator