Theorem ssexg 4433

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 3373	. . . 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 2970	. . . 4 |- x e. _V
4	3	ssex 4431	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3025	. 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 1369   e. wcel 1756   _Vcvv 2967   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337

This theorem is referenced by:  ssexd  4434  difexg  4435  rabexg  4437  elssabg  4442  elpw2g  4450  abssexg  4472  snexALT  4473  sess1  4683  sess2  4684  trsuc  4798  ordsssuc2  4802  riinint  5091  resexg  5144  mptexg  5942  isofr2  6030  ofres  6330  brrpssg  6357  unexb  6375  difex2  6378  uniexb  6381  xpexg  6502  dmexg  6504  rnexg  6505  resiexg  6509  imaexg  6510  exse2  6512  cnvexg  6519  coexg  6523  fabexg  6528  f1oabexg  6531  resfunexgALT  6535  cofunexg  6536  fnexALT  6538  f1dmex  6542  oprabexd  6559  mpt2exxg  6642  suppfnss  6709  tposexg  6754  tz7.48-3  6891  oaabs  7075  erex  7117  mapex  7212  pmvalg  7217  elpmg  7220  elmapssres  7229  pmss12g  7231  ralxpmap  7254  ixpexg  7279  ssdomg  7347  fiprc  7383  domunsncan  7403  infensuc  7481  pssnn  7523  unbnn  7560  fodomfi  7582  fival  7654  fiss  7666  dffi3  7673  hartogslem2  7749  card2on  7761  wdomima2g  7793  unxpwdom2  7795  unxpwdom  7796  harwdom  7797  oemapvali  7884  ackbij1lem11  8391  cofsmo  8430  ssfin4  8471  fin23lem11  8478  ssfin2  8481  ssfin3ds  8491  isfin1-3  8547  hsmex3  8595  axdc2lem  8609  ac6num  8640  zorn2lem1  8657  ttukeylem1  8670  ondomon  8719  fpwwe2lem3  8792  fpwwe2lem12  8800  fpwwe2lem13  8801  canthwe  8810  wuncss  8904  genpv  9160  genpdm  9163  hashss  12158  hashf1lem1  12200  wrdexg  12236  wrdexb  12237  shftfval  12551  o1of2  13082  o1rlimmul  13088  isercolllem2  13135  isstruct2  14175  ressabs  14228  prdsbas  14387  fnmrc  14537  mrcfval  14538  isacs1i  14587  mreacs  14588  isssc  14725  ipolerval  15318  ress0g  15442  symgbas  15876  sylow2a  16109  islbs3  17213  istps3OLD  18502  basdif0  18533  tgval  18535  eltg  18537  eltg2  18538  tgss  18548  basgen2  18569  2basgen  18570  tgdif0  18572  bastop1  18573  resttopon  18740  restabs  18744  restcld  18751  restfpw  18758  restcls  18760  restntr  18761  ordtbas2  18770  ordtbas  18771  lmfval  18811  cnrest  18864  cmpcov  18967  cmpsublem  18977  cmpsub  18978  2ndcomap  19037  txss12  19153  ptrescn  19187  trfbas2  19391  trfbas  19392  isfildlem  19405  snfbas  19414  trfil1  19434  trfil2  19435  trufil  19458  ssufl  19466  hauspwpwf1  19535  ustval  19752  psmetres2  19865  metrest  20074  cnheibor  20502  metcld2  20792  bcthlem1  20810  mbfimaopn2  21110  0pledm  21126  dvbss  21351  dvreslem  21359  dvres2lem  21360  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcnvrelem2  21465  elply2  21639  plyf  21641  plyss  21642  elplyr  21644  plyeq0lem  21653  plyeq0  21654  plyaddlem  21658  plymullem  21659  dgrlem  21672  coeidlem  21680  ulmcn  21839  pserulm  21862  iseupa  23537  issubgo  23741  rabexgfGS  25837  abrexdomjm  25839  dmct  25965  resf1o  25981  ress1r  26208  metidval  26269  indval  26422  sigagenss  26544  measval  26564  omsfval  26661  erdsze2lem1  27043  erdsze2lem2  27044  cvxpcon  27083  dfon2lem3  27549  setlikess  27607  altxpexg  27960  ivthALT  28483  islocfin  28521  filnetlem3  28554  abrexdom  28577  sdclem2  28591  sdclem1  28592  elrfirn  28984  pwssplit4  29395  hbtlem1  29432  hbtlem7  29434  rabexgf  29699  mpt2exxg2  30680  gsumlsscl  30753  lincellss  30849