HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem ssexg 3734
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 2853 . . . 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 2495 . . . 4  |-  x  e.  _V
43ssex 3732 . . 3  |-  ( A  C_  x  ->  A  e.  _V )
52, 4vtoclg 2543 . 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 357    = wceq 1536    e. wcel 1538   _Vcvv 2492    C_ wss 2810
This theorem is referenced by:  difexg  3735  rabexg  3737  elssabg  3739  elpw2g  3740  abssexg  3766  snexALT  3767  sess1  3926  sess2  3927  trsuc  4041  ordsssuc2  4046  unexb  4083  difex2  4088  uniexb  4149  xpexg  4399  riinint  4529  dmexg  4533  rnexg  4534  resexg  4585  resiexg  4588  imaexg  4615  exse2  4636  soex  4702  cnvexg  4785  coexg  4792  fex2  4928  fabexg  4948  f1oabexg  5007  resfunexgALT  5182  cofunexg  5183  fnexALT  5186  mptexg  5189  f1dmex  5195  isofr2  5340  oprabexd  5448  mpt2exg  5450  ofres  5580  fnwelem  5708  fnse  5710  tposexg  5723  brrpssg  5750  tz7.48-3  5903  oaabs  6084  erex  6126  mapex  6211  pmvalg  6216  elpmg  6219  pmss12g  6227  ixpexg  6266  ssdomg  6332  f1imaen2g  6346  fiprc  6366  domunsncan  6386  infensuc  6510  pssnn  6549  unbnn  6576  fodomfi  6598  fival  6628  fiss  6639  dffi3  6646  ordtypelem10  6705  oismo  6718  hartogslem2  6721  wofib  6723  wemapso  6729  card2on  6731  wdom2d  6757  wdomd  6758  wdomima2g  6763  unxpwdom2  6765  unxpwdom  6766  harwdom  6767  cantnfle  6835  cantnflt  6836  cantnflt2  6837  cantnfp1lem2  6844  cantnfp1lem3  6845  oemapvali  6849  cantnflem1b  6851  cantnflem1d  6853  cantnflem1  6854  cnfcomlem  6865  cnfcom  6866  cnfcom2lem  6867  cnfcom3lem  6869  acni2  7135  ackbij1lem11  7299  cofsmo  7338  ssfin4  7379  fin23lem11  7386  ssfin2  7389  ssfin3ds  7399  isfin1-3  7455  fin1a2lem12  7480  hsmexlem1  7495  hsmex3  7503  axdc2lem  7517  ac6num  7544  zorn2lem1  7579  zorn2lem4  7582  ttukeylem1  7592  ondomon  7639  fpwwe2lem2  7706  fpwwe2lem3  7707  fpwwe2lem5  7708  fpwwe2lem12  7715  fpwwe2lem13  7716  fpwwe2  7717  fpwwelem  7719  canthwelem  7724  canthwe  7725  pwfseqlem4  7735  genpv  8023  genpdm  8026  hashf1lem1  10302  shftfval  10316  o1of2  10685  o1rlimmul  10690  isercolllem2  10721  hashbcss  11506  isstruct2  11611  strssd  11631  ressbas2  11647  ressabs  11654  restid2  11767  prdsbas  11787  divsfval  11877  ipolerval  12112  sswrd  12302  frmdsssubm  12395  frmdss2  12397  eqgfval  12574  gass  12659  symgbas  12676  sylow2a  12759  sylow2blem2  12761  islbs3  13586  mplsubglem  13853  mpllsslem  13854  opsrtoslem2  13900  fnmrc  14315  mrcfval  14316  isacs1i  14350  mreacs  14351  istps3OLD  14403  basdif0  14434  tgval  14436  eltg  14438  eltg2  14439  tgss  14449  basgen2  14470  2basgen  14471  tgdif0  14473  bastop1  14474  resttopon  14612  restabs  14616  restcld  14623  restfpw  14630  restcls  14631  restntr  14632  lpval  14638  ordtbaslem  14646  ordtbas2  14649  ordtbas  14650  ordtrest2  14662  lmfval  14690  cnrest  14741  cnrest2  14742  cnpresti  14744  cnprest  14745  cnprest2  14746  cmpcov  14841  cmpsublem  14851  cmpsub  14852  consuba  14871  consubclo  14875  uncon  14880  2ndcomap  14908  1stcelcls  14911  hausmapdom  14950  ptbasfi  15000  txss12  15024  ptcls  15034  ptrescn  15057  cnmpt2res  15095  qtopval2  15111  elqtop  15112  qtoprest  15132  ptuncnv  15222  ptunhmeo  15223  trfbas2  15262  trfbas  15263  isfildlem  15276  snfbas  15285  fsubbas  15286  trfil1  15305  trfil2  15306  trufil  15329  ssufl  15337  elfm  15366  rnelfmlem  15371  rnelfm  15372  fmfnfmlem4  15376  flimclslem  15403  hauspwpwf1  15406  hauspwpwdom  15407  ptcmplem1  15470  xmetres2  15649  metrest  15795  cnheibor  16171  fmcfil  16414  metcld2  16448  bcthlem1  16462  mbfimaopn2  16728  0pledm  16744  dvfval  16936  dvbss  16941  dvlmlem1  16943  dvlmlem2  16944  dvlm  16945  dvreslem  16952  dvres2lem  16953  dvcnp2  16962  dvnf  16968  dvnbss  16969  dvaddbr  16978  dvmulbr  16979  dvaddf  16982  dvmulf  16983  dvcmulf  16985  dvcof  16988  dvcnvrelem2  17040  elply2  17236  plyf  17238  plyss  17239  elplyr  17241  plyeq0lem  17250  plyeq0  17251  plyaddlem  17255  plymullem  17256  dgrlem  17269  coeidlem  17277  ulmss  17377  ulmcn  17379  pserulm  17401  issubgo  18191  erdsze2lem1  20296  erdsze2lem2  20297  cvxpcon  20340  cvmliftmolem1  20379  iseupa  20447  dfon2lem3  20731  setlikess  20789  altxpexg  21111  oprabex2gpop  21573  sndw  21641  prjmapcp  21710  prjmapcp2  21715  ubpar  21806  qusp  22093  efilcp  22103  cnfilca  22107  islimrs3  22132  islimrs4  22133  fnctartar3  22462  prismorcsetlem  22465  prismorcset  22467  isline1  22539  lemindclsbu  22584  indcls2  22585  ivthALT  22704  islocfin  22742  neibastop2lem  22755  fnejoin1  22763  filnetlem3  22775  filnetlem4  22776  abrexdom  22853  sdclem2  22900  sdclem1  22901  ralxpmap  23212  elrfi  23220  elrfirn  23221  elrfirn2  23222  elmapssres  23243  pwssplit0  23715  pwssplit1  23716  pwssplit2  23717  pwssplit3  23718  pwssplit4  23719  frlmsplit2  23771  frlmsslss  23772  islinds2  23811  hbtlem1  23855  hbtlem7  23857  pmtrfconj  23935  bnj74  25060  bnj1412  26131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606  ax-16 1793  ax-ext 2064  ax-sep 3715
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-ex 1456  df-sb 1754  df-clab 2070  df-cleq 2075  df-clel 2078  df-v 2494  df-in 2817  df-ss 2821
Copyright terms: Public domain