Theorem ssexg 4583

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.

Step	Hyp	Ref	Expression
1		sseq2 3511	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 317	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 3098	. . . 4 |- x e. _V
4	3	ssex 4581	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3153	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 430	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1383   e. wcel 1804   _Vcvv 3095   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475

This theorem is referenced by:  ssexd  4584  difexg  4585  rabexg  4587  elssabg  4592  elpw2g  4600  abssexg  4622  snexALT  4623  sess1  4837  sess2  4838  trsuc  4952  ordsssuc2  4956  riinint  5249  resexg  5306  mptexg  6127  isofr2  6225  ofres  6540  brrpssg  6567  unexb  6585  xpexg  6587  difex2  6592  uniexb  6595  dmexg  6716  rnexg  6717  resiexg  6721  imaexg  6722  exse2  6724  cnvexg  6731  coexg  6736  fabexg  6741  f1oabexg  6744  resfunexgALT  6748  cofunexg  6749  fnexALT  6751  f1dmex  6755  oprabexd  6772  mpt2exxg  6859  suppfnss  6927  tposexg  6971  tz7.48-3  7111  oaabs  7295  erex  7337  mapex  7428  pmvalg  7433  elpmg  7436  elmapssres  7445  pmss12g  7447  ralxpmap  7470  ixpexg  7495  ssdomg  7563  fiprc  7599  domunsncan  7619  infensuc  7697  pssnn  7740  unbnn  7778  fodomfi  7801  fival  7874  fiss  7886  dffi3  7893  hartogslem2  7971  card2on  7983  wdomima2g  8015  unxpwdom2  8017  unxpwdom  8018  harwdom  8019  oemapvali  8106  ackbij1lem11  8613  cofsmo  8652  ssfin4  8693  fin23lem11  8700  ssfin2  8703  ssfin3ds  8713  isfin1-3  8769  hsmex3  8817  axdc2lem  8831  ac6num  8862  ttukeylem1  8892  ondomon  8941  fpwwe2lem3  9014  fpwwe2lem12  9022  fpwwe2lem13  9023  canthwe  9032  wuncss  9126  genpv  9380  genpdm  9383  hashss  12456  hashf1lem1  12486  wrdexg  12539  wrdexb  12540  shftfval  12885  o1of2  13417  o1rlimmul  13423  isercolllem2  13470  isstruct2  14623  ressabs  14677  prdsbas  14836  fnmrc  14986  mrcfval  14987  isacs1i  15036  mreacs  15037  isssc  15171  ipolerval  15765  ress0g  15928  symgbas  16384  sylow2a  16618  islbs3  17780  istps3OLD  19401  basdif0  19432  tgval  19434  eltg  19436  eltg2  19437  tgss  19448  basgen2  19469  2basgen  19470  bastop1  19473  resttopon  19640  restabs  19644  restcld  19651  restfpw  19658  restcls  19660  restntr  19661  ordtbas2  19670  ordtbas  19671  lmfval  19711  cnrest  19764  cmpcov  19867  cmpsublem  19877  cmpsub  19878  2ndcomap  19937  islocfin  19996  txss12  20084  ptrescn  20118  trfbas2  20322  trfbas  20323  isfildlem  20336  snfbas  20345  trfil1  20365  trfil2  20366  trufil  20389  ssufl  20397  hauspwpwf1  20466  ustval  20683  metrest  21005  cnheibor  21433  metcld2  21723  bcthlem1  21741  mbfimaopn2  22042  0pledm  22058  dvbss  22283  dvreslem  22291  dvres2lem  22292  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcnvrelem2  22397  elply2  22571  plyf  22573  plyss  22574  elplyr  22576  plyeq0lem  22585  plyeq0  22586  plyaddlem  22590  plymullem  22591  dgrlem  22604  coeidlem  22612  ulmcn  22772  pserulm  22795  iseupa  24943  issubgo  25283  rabexgfGS  27379  abrexdomjm  27383  dmct  27515  ress1r  27757  pcmplfin  27841  metidval  27847  indval  28005  sigagenss  28127  measval  28147  erdsze2lem1  28625  erdsze2lem2  28626  cvxpcon  28665  elmsta  28886  dfon2lem3  29193  setlikess  29251  altxpexg  29604  ivthALT  30129  filnetlem3  30174  abrexdom  30197  sdclem2  30211  sdclem1  30212  elrfirn  30603  pwssplit4  31011  hbtlem1  31048  hbtlem7  31050  rabexgf  31353  dvnprodlem1  31697  dvnprodlem2  31698  ressval3d  32509  mpt2exxg2  32795  gsumlsscl  32846  lincellss  32897