Theorem ssexg 4309

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 3330	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 309	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 2919	. . . 4 |- x e. _V
4	3	ssex 4307	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2971	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 420	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   _Vcvv 2916   C_ wss 3280

This theorem is referenced by:  ssexd  4310  difexg  4311  rabexg  4313  elssabg  4315  elpw2g  4323  abssexg  4344  snexALT  4345  sess1  4510  sess2  4511  trsuc  4625  ordsssuc2  4629  unexb  4668  difex2  4673  uniexb  4711  xpexg  4948  riinint  5085  dmexg  5089  rnexg  5090  resexg  5144  resiexg  5147  imaexg  5176  exse2  5197  cnvexg  5364  coexg  5371  fabexg  5583  f1oabexg  5645  resfunexgALT  5917  cofunexg  5918  fnexALT  5921  mptexg  5924  f1dmex  5930  isofr2  6023  oprabexd  6145  ofres  6280  mpt2exxg  6381  tposexg  6452  brrpssg  6483  tz7.48-3  6660  oaabs  6846  erex  6888  mapex  6983  pmvalg  6988  elpmg  6991  pmss12g  6999  ixpexg  7045  ssdomg  7112  fiprc  7147  domunsncan  7167  infensuc  7244  pssnn  7286  unbnn  7322  fodomfi  7344  fival  7375  fiss  7387  dffi3  7394  hartogslem2  7468  card2on  7478  wdomima2g  7510  unxpwdom2  7512  unxpwdom  7513  harwdom  7514  oemapvali  7596  ackbij1lem11  8066  cofsmo  8105  ssfin4  8146  fin23lem11  8153  ssfin2  8156  ssfin3ds  8166  isfin1-3  8222  hsmex3  8270  axdc2lem  8284  ac6num  8315  zorn2lem1  8332  ttukeylem1  8345  ondomon  8394  fpwwe2lem3  8464  fpwwe2lem12  8472  fpwwe2lem13  8473  canthwe  8482  wuncss  8576  genpv  8832  genpdm  8835  hashf1lem1  11659  wrdexg  11694  wrdexb  11718  shftfval  11840  o1of2  12361  o1rlimmul  12367  isercolllem2  12414  isstruct2  13433  ressabs  13482  prdsbas  13635  fnmrc  13787  mrcfval  13788  isacs1i  13837  mreacs  13838  isssc  13975  ipolerval  14537  symgbas  15050  sylow2a  15208  islbs3  16182  istps3OLD  16942  basdif0  16973  tgval  16975  eltg  16977  eltg2  16978  tgss  16988  basgen2  17009  2basgen  17010  tgdif0  17012  bastop1  17013  resttopon  17179  restabs  17183  restcld  17190  restfpw  17197  restcls  17199  restntr  17200  ordtbas2  17209  ordtbas  17210  lmfval  17250  cnrest  17303  cmpcov  17406  cmpsublem  17416  cmpsub  17417  2ndcomap  17474  txss12  17590  ptrescn  17624  trfbas2  17828  trfbas  17829  isfildlem  17842  snfbas  17851  trfil1  17871  trfil2  17872  trufil  17895  ssufl  17903  hauspwpwf1  17972  ustval  18185  psmetres2  18298  metrest  18507  cnheibor  18933  metcld2  19212  bcthlem1  19230  mbfimaopn2  19502  0pledm  19518  dvbss  19741  dvreslem  19749  dvres2lem  19750  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcnvrelem2  19855  elply2  20068  plyf  20070  plyss  20071  elplyr  20073  plyeq0lem  20082  plyeq0  20083  plyaddlem  20087  plymullem  20088  dgrlem  20101  coeidlem  20109  ulmcn  20268  pserulm  20291  iseupa  21640  issubgo  21844  rabexgfGS  23940  abrexdomjm  23941  dmct  24059  ress0g  24135  metidval  24238  indval  24364  sigagenss  24485  measval  24505  erdsze2lem1  24842  erdsze2lem2  24843  cvxpcon  24882  dfon2lem3  25355  setlikess  25409  altxpexg  25727  ivthALT  26228  islocfin  26266  filnetlem3  26299  abrexdom  26322  sdclem2  26336  sdclem1  26337  ralxpmap  26632  elrfirn  26639  elmapssres  26661  pwssplit4  27059  hbtlem1  27195  hbtlem7  27197  rabexgf  27562

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294