Theorem ssexg 4426

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 3366	. . . 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 2965	. . . 4 |- x e. _V
4	3	ssex 4424	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3019	. 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 1362   e. wcel 1755   _Vcvv 2962   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330

This theorem is referenced by:  ssexd  4427  difexg  4428  rabexg  4430  elssabg  4435  elpw2g  4443  abssexg  4465  snexALT  4466  sess1  4675  sess2  4676  trsuc  4790  ordsssuc2  4794  riinint  5083  resexg  5137  mptexg  5934  isofr2  6022  ofres  6324  brrpssg  6351  unexb  6369  difex2  6372  uniexb  6375  xpexg  6496  dmexg  6498  rnexg  6499  resiexg  6503  imaexg  6504  exse2  6506  cnvexg  6513  coexg  6517  fabexg  6522  f1oabexg  6525  resfunexgALT  6529  cofunexg  6530  fnexALT  6532  f1dmex  6536  oprabexd  6553  mpt2exxg  6636  suppfnss  6703  tposexg  6748  tz7.48-3  6885  oaabs  7071  erex  7113  mapex  7208  pmvalg  7213  elpmg  7216  elmapssres  7225  pmss12g  7227  ralxpmap  7250  ixpexg  7275  ssdomg  7343  fiprc  7379  domunsncan  7399  infensuc  7477  pssnn  7519  unbnn  7556  fodomfi  7578  fival  7650  fiss  7662  dffi3  7669  hartogslem2  7745  card2on  7757  wdomima2g  7789  unxpwdom2  7791  unxpwdom  7792  harwdom  7793  oemapvali  7880  ackbij1lem11  8387  cofsmo  8426  ssfin4  8467  fin23lem11  8474  ssfin2  8477  ssfin3ds  8487  isfin1-3  8543  hsmex3  8591  axdc2lem  8605  ac6num  8636  zorn2lem1  8653  ttukeylem1  8666  ondomon  8715  fpwwe2lem3  8788  fpwwe2lem12  8796  fpwwe2lem13  8797  canthwe  8806  wuncss  8900  genpv  9156  genpdm  9159  hashss  12150  hashf1lem1  12192  wrdexg  12228  wrdexb  12229  shftfval  12543  o1of2  13074  o1rlimmul  13080  isercolllem2  13127  isstruct2  14166  ressabs  14219  prdsbas  14378  fnmrc  14528  mrcfval  14529  isacs1i  14578  mreacs  14579  isssc  14716  ipolerval  15309  ress0g  15433  symgbas  15865  sylow2a  16098  islbs3  17158  istps3OLD  18369  basdif0  18400  tgval  18402  eltg  18404  eltg2  18405  tgss  18415  basgen2  18436  2basgen  18437  tgdif0  18439  bastop1  18440  resttopon  18607  restabs  18611  restcld  18618  restfpw  18625  restcls  18627  restntr  18628  ordtbas2  18637  ordtbas  18638  lmfval  18678  cnrest  18731  cmpcov  18834  cmpsublem  18844  cmpsub  18845  2ndcomap  18904  txss12  19020  ptrescn  19054  trfbas2  19258  trfbas  19259  isfildlem  19272  snfbas  19281  trfil1  19301  trfil2  19302  trufil  19325  ssufl  19333  hauspwpwf1  19402  ustval  19619  psmetres2  19732  metrest  19941  cnheibor  20369  metcld2  20659  bcthlem1  20677  mbfimaopn2  20977  0pledm  20993  dvbss  21218  dvreslem  21226  dvres2lem  21227  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcnvrelem2  21332  elply2  21549  plyf  21551  plyss  21552  elplyr  21554  plyeq0lem  21563  plyeq0  21564  plyaddlem  21568  plymullem  21569  dgrlem  21582  coeidlem  21590  ulmcn  21749  pserulm  21772  iseupa  23409  issubgo  23613  rabexgfGS  25710  abrexdomjm  25712  dmct  25838  resf1o  25855  ress1r  26110  metidval  26171  indval  26324  sigagenss  26446  measval  26466  erdsze2lem1  26939  erdsze2lem2  26940  cvxpcon  26979  dfon2lem3  27445  setlikess  27503  altxpexg  27856  ivthALT  28374  islocfin  28412  filnetlem3  28445  abrexdom  28468  sdclem2  28482  sdclem1  28483  elrfirn  28876  pwssplit4  29287  hbtlem1  29324  hbtlem7  29326  rabexgf  29591  mpt2exxg2  30572  gsumlsscl  30625  lincellss  30669