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

Theorem ssexg 3718
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 2834 . . . 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 2476 . . . 4  |-  x  e. 
_V
43ssex 3716 . . 3  |-  ( A 
C_  x  ->  A  e.  _V )
52, 4vtoclg 2524 . 2  |-  ( B  e.  C  ->  ( A  C_  B  ->  A  e.  _V ) )
65impcom 415 1  |-  ( ( A  C_  B  /\  B  e.  C )  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 356    = wceq 1518    e. wcel 1520   _Vcvv 2473    C_ wss 2791
This theorem is referenced by:  difexg  3719  rabexg  3721  elssabg  3723  elpw2g  3724  abssexg  3750  snexALT  3751  sess1  3910  sess2  3911  trsuc  4025  ordsssuc2  4030  unexb  4067  difex2  4072  uniexb  4128  xpexg  4380  riinint  4515  dmexg  4519  rnexg  4520  resexg  4574  resiexg  4577  imaexg  4605  exse2  4626  soex  4701  cnvexg  4784  coexg  4791  fex2  4927  fabexg  4947  f1oabexg  5006  resfunexgALT  5183  cofunexg  5184  fnexALT  5187  mptexg  5190  f1dmex  5196  isofr2  5342  oprabexd  5451  mpt2exg  5453  ofres  5582  fnwelem  5711  fnse  5713  tposexg  5727  brrpssg  5754  tz7.48-3  5907  oaabs  6093  erex  6135  mapex  6219  pmvalg  6224  elpmg  6227  pmss12g  6235  ixpexg  6275  ssdomg  6341  f1imaen2g  6355  fiprc  6375  domunsncan  6395  infensuc  6519  pssnn  6560  unbnn  6592  fodomfi  6614  fival  6644  fiss  6655  dffi3  6662  ordtypelem10  6721  oismo  6734  hartogslem2  6737  wofib  6739  wemapso  6745  card2on  6747  wdom2d  6773  wdomd  6774  wdomima2g  6779  unxpwdom2  6781  unxpwdom  6782  harwdom  6783  cantnfle  6851  cantnflt  6852  cantnflt2  6853  cantnfp1lem2  6860  cantnfp1lem3  6861  oemapvali  6865  cantnflem1b  6867  cantnflem1d  6869  cantnflem1  6870  cnfcomlem  6881  cnfcom  6882  cnfcom2lem  6883  cnfcom3lem  6885  acni2  7151  ackbij1lem11  7315  cofsmo  7354  ssfin4  7395  fin23lem11  7402  ssfin2  7405  ssfin3ds  7415  isfin1-3  7471  fin1a2lem12  7496  hsmexlem1  7511  hsmex3  7519  axdc2lem  7533  ac6num  7560  zorn2lem1  7595  zorn2lem4  7598  ttukeylem1  7608  ondomon  7655  fpwwe2lem2  7722  fpwwe2lem3  7723  fpwwe2lem5  7724  fpwwe2lem12  7731  fpwwe2lem13  7732  fpwwe2  7733  fpwwelem  7735  canthwelem  7740  canthwe  7741  pwfseqlem4  7751  genpv  8039  genpdm  8042  hashf1lem1  10355  shftfval  10369  o1of2  10772  o1rlimmul  10778  isercolllem2  10810  hashbcss  11622  isstruct2  11727  strssd  11748  ressabs  11771  restid2  11889  prdsbas  11909  divsfval  11999  fnmrc  12057  mrcfval  12058  isacs1i  12079  mreacs  12080  ipolerval  12285  wrdexg  12490  wrdexb  12514  gass  12930  symgbas  12947  sylow2a  13105  sylow2blem2  13107  dprdres  13435  islbs3  14078  mplsubglem  14348  mpllsslem  14349  opsrtoslem2  14395  istps3OLD  14829  basdif0  14860  tgval  14862  eltg  14864  eltg2  14865  tgss  14875  basgen2  14896  2basgen  14897  tgdif0  14899  bastop1  14900  resttopon  15038  restabs  15042  restcld  15049  restfpw  15056  restcls  15057  restntr  15058  lpval  15064  ordtbaslem  15072  ordtbas2  15075  ordtbas  15076  ordtrest2  15088  lmfval  15116  cnrest  15167  cnrest2  15168  cnpresti  15170  cnprest  15171  cnprest2  15172  cmpcov  15267  cmpsublem  15277  cmpsub  15278  consuba  15297  consubclo  15301  uncon  15306  2ndcomap  15334  1stcelcls  15337  hausmapdom  15376  ptbasfi  15426  txss12  15450  ptcls  15460  ptrescn  15483  cnmpt2res  15521  qtopval2  15537  elqtop  15538  qtoprest  15558  ptuncnv  15648  ptunhmeo  15649  trfbas2  15688  trfbas  15689  isfildlem  15702  snfbas  15711  fsubbas  15712  trfil1  15731  trfil2  15732  trufil  15755  ssufl  15763  elfm  15792  rnelfmlem  15797  rnelfm  15798  fmfnfmlem4  15802  flimclslem  15829  hauspwpwf1  15832  hauspwpwdom  15833  ptcmplem1  15896  xmetres2  16075  metrest  16221  cnheibor  16597  fmcfil  16840  metcld2  16874  bcthlem1  16888  mbfimaopn2  17154  0pledm  17170  dvfval  17362  dvbss  17367  dvlmlem1  17369  dvlmlem2  17370  dvlm  17371  dvreslem  17378  dvres2lem  17379  dvcnp2  17388  dvnf  17394  dvnbss  17395  dvaddbr  17404  dvmulbr  17405  dvaddf  17408  dvmulf  17409  dvcmulf  17411  dvcof  17414  dvcnvrelem2  17467  elply2  17663  plyf  17665  plyss  17666  elplyr  17668  plyeq0lem  17677  plyeq0  17678  plyaddlem  17682  plymullem  17683  dgrlem  17696  coeidlem  17704  ulmss  17804  ulmcn  17806  pserulm  17828  issubgo  18793  erdsze2lem1  20898  erdsze2lem2  20899  cvxpcon  20937  cvmliftmolem1  20976  iseupa  21045  dfon2lem3  21303  setlikess  21359  altxpexg  21681  oprabex2gpop  22143  sndw  22207  prjmapcp  22274  prjmapcp2  22279  ubpar  22370  qusp  22657  efilcp  22667  cnfilca  22671  islimrs3  22696  islimrs4  22697  fnctartar3  23024  prismorcsetlem  23027  prismorcset  23029  lemindclsbu  23108  indcls2  23109  ivthALT  23324  islocfin  23362  neibastop2lem  23375  fnejoin1  23383  filnetlem3  23395  filnetlem4  23396  abrexdom  23472  sdclem2  23519  sdclem1  23520  ralxpmap  23830  elrfi  23838  elrfirn  23839  elrfirn2  23840  elmapssres  23861  pwssplit0  24297  pwssplit1  24298  pwssplit2  24299  pwssplit3  24300  pwssplit4  24301  frlmsplit2  24353  frlmsslss  24354  hbtlem1  24437  hbtlem7  24439  pmtrfconj  24517  bnj74  25611  bnj1412  26682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587  ax-16 1773  ax-ext 2044  ax-sep 3699
This theorem depends on definitions:  df-bi 175  df-or 357  df-an 358  df-ex 1445  df-sb 1734  df-clab 2050  df-cleq 2055  df-clel 2058  df-v 2475  df-in 2798  df-ss 2802
Copyright terms: Public domain