Theorem ssexg 4593

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 3526	. . . 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 3116	. . . 4 |- x e. _V
4	3	ssex 4591	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3171	. 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 1379   e. wcel 1767   _Vcvv 3113   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490

This theorem is referenced by:  ssexd  4594  difexg  4595  rabexg  4597  elssabg  4602  elpw2g  4610  abssexg  4632  snexALT  4633  sess1  4847  sess2  4848  trsuc  4962  ordsssuc2  4966  riinint  5258  resexg  5315  mptexg  6129  isofr2  6227  ofres  6538  brrpssg  6565  unexb  6583  difex2  6586  uniexb  6589  xpexg  6710  dmexg  6715  rnexg  6716  resiexg  6720  imaexg  6721  exse2  6723  cnvexg  6730  coexg  6735  fabexg  6740  f1oabexg  6743  resfunexgALT  6747  cofunexg  6748  fnexALT  6750  f1dmex  6754  oprabexd  6771  mpt2exxg  6857  suppfnss  6925  tposexg  6969  tz7.48-3  7109  oaabs  7293  erex  7335  mapex  7426  pmvalg  7431  elpmg  7434  elmapssres  7443  pmss12g  7445  ralxpmap  7468  ixpexg  7493  ssdomg  7561  fiprc  7597  domunsncan  7617  infensuc  7695  pssnn  7738  unbnn  7775  fodomfi  7798  fival  7871  fiss  7883  dffi3  7890  hartogslem2  7967  card2on  7979  wdomima2g  8011  unxpwdom2  8013  unxpwdom  8014  harwdom  8015  oemapvali  8102  ackbij1lem11  8609  cofsmo  8648  ssfin4  8689  fin23lem11  8696  ssfin2  8699  ssfin3ds  8709  isfin1-3  8765  hsmex3  8813  axdc2lem  8827  ac6num  8858  zorn2lem1  8875  ttukeylem1  8888  ondomon  8937  fpwwe2lem3  9010  fpwwe2lem12  9018  fpwwe2lem13  9019  canthwe  9028  wuncss  9122  genpv  9376  genpdm  9379  hashss  12438  hashf1lem1  12469  wrdexg  12522  wrdexb  12523  shftfval  12865  o1of2  13397  o1rlimmul  13403  isercolllem2  13450  isstruct2  14498  ressabs  14552  prdsbas  14711  fnmrc  14861  mrcfval  14862  isacs1i  14911  mreacs  14912  isssc  15049  ipolerval  15642  ress0g  15767  symgbas  16207  sylow2a  16442  islbs3  17596  istps3OLD  19206  basdif0  19237  tgval  19239  eltg  19241  eltg2  19242  tgss  19252  basgen2  19273  2basgen  19274  tgdif0  19276  bastop1  19277  resttopon  19444  restabs  19448  restcld  19455  restfpw  19462  restcls  19464  restntr  19465  ordtbas2  19474  ordtbas  19475  lmfval  19515  cnrest  19568  cmpcov  19671  cmpsublem  19681  cmpsub  19682  2ndcomap  19741  txss12  19857  ptrescn  19891  trfbas2  20095  trfbas  20096  isfildlem  20109  snfbas  20118  trfil1  20138  trfil2  20139  trufil  20162  ssufl  20170  hauspwpwf1  20239  ustval  20456  psmetres2  20569  metrest  20778  cnheibor  21206  metcld2  21496  bcthlem1  21514  mbfimaopn2  21815  0pledm  21831  dvbss  22056  dvreslem  22064  dvres2lem  22065  dvcnp2  22074  dvaddbr  22092  dvmulbr  22093  dvcnvrelem2  22170  elply2  22344  plyf  22346  plyss  22347  elplyr  22349  plyeq0lem  22358  plyeq0  22359  plyaddlem  22363  plymullem  22364  dgrlem  22377  coeidlem  22385  ulmcn  22544  pserulm  22567  perpln1  23811  perpln2  23812  isperp  23813  iseupa  24657  issubgo  24997  rabexgfGS  27093  abrexdomjm  27095  dmct  27225  resf1o  27241  ress1r  27458  metidval  27521  indval  27683  sigagenss  27805  measval  27825  omsfval  27921  erdsze2lem1  28303  erdsze2lem2  28304  cvxpcon  28343  dfon2lem3  28810  setlikess  28868  altxpexg  29221  ivthALT  29746  islocfin  29784  filnetlem3  29817  abrexdom  29840  sdclem2  29854  sdclem1  29855  elrfirn  30247  pwssplit4  30655  hbtlem1  30692  hbtlem7  30694  rabexgf  30993  limsupre  31199  mpt2exxg2  32011  gsumlsscl  32066  lincellss  32117