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

Theorem ssexg 4176
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 3213 . . . 4  |-  ( x  =  B  ->  ( A  C_  x  <->  A  C_  B
) )
21imbi1d 308 . . 3  |-  ( x  =  B  ->  (
( A  C_  x  ->  A  e.  _V )  <->  ( A  C_  B  ->  A  e.  _V ) ) )
3 vex 2804 . . . 4  |-  x  e. 
_V
43ssex 4174 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2856 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 419 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696   _Vcvv 2801    C_ wss 3165
This theorem is referenced by:  ssexd  4177  difexg  4178  rabexg  4180  elssabg  4182  elpw2g  4190  abssexg  4211  snexALT  4212  sess1  4377  sess2  4378  trsuc  4492  ordsssuc2  4497  unexb  4536  difex2  4541  uniexb  4579  xpexg  4816  riinint  4951  dmexg  4955  rnexg  4956  resexg  5010  resiexg  5013  imaexg  5042  exse2  5063  soex  5138  cnvexg  5224  coexg  5231  fex2  5417  fabexg  5438  f1oabexg  5500  resfunexgALT  5754  cofunexg  5755  fnexALT  5758  mptexg  5761  f1dmex  5767  isofr2  5857  oprabexd  5976  ofres  6110  mpt2exxg  6211  fnwelem  6246  fnse  6248  tposexg  6264  brrpssg  6295  tz7.48-3  6472  oaabs  6658  erex  6700  mapex  6794  pmvalg  6799  elpmg  6802  pmss12g  6810  ixpexg  6856  ssdomg  6923  f1imaen2g  6938  fiprc  6958  domunsncan  6978  infensuc  7055  pssnn  7097  unbnn  7129  fodomfi  7151  fival  7182  fiss  7193  dffi3  7200  ordtypelem10  7258  oismo  7271  hartogslem2  7274  wofib  7276  wemapso  7282  card2on  7284  wdom2d  7310  wdomd  7311  wdomima2g  7316  unxpwdom2  7318  unxpwdom  7319  harwdom  7320  cantnfle  7388  cantnflt  7389  cantnflt2  7390  cantnfp1lem2  7397  cantnfp1lem3  7398  oemapvali  7402  cantnflem1b  7404  cantnflem1d  7406  cantnflem1  7407  cnfcomlem  7418  cnfcom  7419  cnfcom2lem  7420  cnfcom3lem  7422  acni2  7689  ackbij1lem11  7872  cofsmo  7911  ssfin4  7952  fin23lem11  7959  ssfin2  7962  ssfin3ds  7972  isfin1-3  8028  fin1a2lem12  8053  hsmexlem1  8068  hsmex3  8076  axdc2lem  8090  ac6num  8122  zorn2lem1  8139  zorn2lem4  8142  ttukeylem1  8152  ondomon  8201  fpwwe2lem2  8270  fpwwe2lem3  8271  fpwwe2lem5  8272  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  fpwwelem  8283  canthwelem  8288  canthwe  8289  pwfseqlem4  8300  wuncss  8383  genpv  8639  genpdm  8642  hashf1lem1  11409  wrdexg  11441  wrdexb  11465  shftfval  11581  o1of2  12102  o1rlimmul  12108  isercolllem2  12155  hashbcss  13067  isstruct2  13173  strssd  13198  ressabs  13222  restid2  13351  prdsbas  13373  divsfval  13465  fnmrc  13525  mrcfval  13526  isacs1i  13575  mreacs  13576  isssc  13713  rescabs  13726  rescabs2  13727  resssetc  13940  resscatc  13953  yonedalem1  14062  yonedalem21  14063  yonedalem3a  14064  yonedalem4c  14067  yonedalem22  14068  yonedalem3b  14069  yonedainv  14071  yonffthlem  14072  ipolerval  14275  gass  14771  symgbas  14788  sylow2a  14946  sylow2blem2  14948  dprdres  15279  islbs3  15924  mplsubglem  16195  mpllsslem  16196  opsrtoslem2  16242  istps3OLD  16676  basdif0  16707  tgval  16709  eltg  16711  eltg2  16712  tgss  16722  basgen2  16743  2basgen  16744  tgdif0  16746  bastop1  16747  lpval  16887  resttopon  16908  restabs  16912  restcld  16919  restfpw  16926  restcls  16927  restntr  16928  ordtbaslem  16934  ordtbas2  16937  ordtbas  16938  ordtrest2  16950  lmfval  16978  cnrest  17029  cnrest2  17030  cnpresti  17032  cnprest  17033  cnprest2  17034  cmpcov  17132  cmpsublem  17142  cmpsub  17143  consuba  17162  consubclo  17166  uncon  17171  2ndcomap  17200  1stcelcls  17203  hausmapdom  17242  ptbasfi  17292  txss12  17316  ptcls  17326  ptrescn  17349  cnmpt2res  17387  qtopval2  17403  elqtop  17404  qtoprest  17424  ptuncnv  17514  ptunhmeo  17515  trfbas2  17554  trfbas  17555  isfildlem  17568  snfbas  17577  fsubbas  17578  trfil1  17597  trfil2  17598  trufil  17621  ssufl  17629  elfm  17658  rnelfmlem  17663  rnelfm  17664  fmfnfmlem4  17668  flimclslem  17695  hauspwpwf1  17698  hauspwpwdom  17699  ptcmplem1  17762  xmetres2  17941  metrest  18086  cnheibor  18469  fmcfil  18714  metcld2  18748  bcthlem1  18762  mbfimaopn2  19028  0pledm  19044  dvbss  19267  dvreslem  19275  dvres2lem  19276  dvcnp2  19285  dvnf  19292  dvnbss  19293  dvaddbr  19303  dvmulbr  19304  dvaddf  19307  dvmulf  19308  dvcmulf  19310  dvcof  19313  dvcnvrelem2  19381  elply2  19594  plyf  19596  plyss  19597  elplyr  19599  plyeq0lem  19608  plyeq0  19609  plyaddlem  19613  plymullem  19614  dgrlem  19627  coeidlem  19635  ulmss  19790  ulmcn  19792  pserulm  19814  issubgo  20986  abrexdomjm  23181  rabexgfGS  23187  dmct  23357  lmlim  23386  esumpinfval  23456  sigagenss  23525  measbase  23543  measval  23544  ismeas  23545  indval  23612  erdsze2lem1  23749  erdsze2lem2  23750  cvxpcon  23788  cvmliftmolem1  23827  iseupa  23896  dfon2lem3  24211  setlikess  24265  altxpexg  24583  oprabex2gpop  25138  sndw  25202  prjmapcp  25267  prjmapcp2  25272  ubpar  25363  qusp  25644  efilcp  25654  cnfilca  25658  islimrs3  25683  islimrs4  25684  fnctartar3  26011  prismorcsetlem  26014  prismorcset  26016  lemindclsbu  26097  indcls2  26098  ivthALT  26360  islocfin  26398  neibastop2lem  26411  fnejoin1  26419  filnetlem3  26431  filnetlem4  26432  abrexdom  26507  sdclem2  26554  sdclem1  26555  ralxpmap  26863  elrfi  26871  elrfirn  26872  elrfirn2  26873  elmapssres  26894  pwssplit0  27289  pwssplit1  27290  pwssplit2  27291  pwssplit3  27292  pwssplit4  27293  frlmsplit2  27345  frlmsslss  27346  hbtlem1  27429  hbtlem7  27431  pmtrfconj  27509  rabexgf  27797  stoweidlem31  27882  stoweidlem53  27904  stoweidlem57  27908  stoweidlem59  27910  bnj1413  29380
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator