Theorem ssexg 4549

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 3489	. . . 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 3081	. . . 4 |- x e. _V
4	3	ssex 4547	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3136	. 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 1370   e. wcel 1758   _Vcvv 3078   C_ wss 3439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446  df-ss 3453

This theorem is referenced by:  ssexd  4550  difexg  4551  rabexg  4553  elssabg  4558  elpw2g  4566  abssexg  4588  snexALT  4589  sess1  4799  sess2  4800  trsuc  4914  ordsssuc2  4918  riinint  5207  resexg  5260  mptexg  6059  isofr2  6147  ofres  6448  brrpssg  6475  unexb  6493  difex2  6496  uniexb  6499  xpexg  6620  dmexg  6622  rnexg  6623  resiexg  6627  imaexg  6628  exse2  6630  cnvexg  6637  coexg  6641  fabexg  6646  f1oabexg  6649  resfunexgALT  6653  cofunexg  6654  fnexALT  6656  f1dmex  6660  oprabexd  6677  mpt2exxg  6760  suppfnss  6827  tposexg  6872  tz7.48-3  7012  oaabs  7196  erex  7238  mapex  7333  pmvalg  7338  elpmg  7341  elmapssres  7350  pmss12g  7352  ralxpmap  7375  ixpexg  7400  ssdomg  7468  fiprc  7504  domunsncan  7524  infensuc  7602  pssnn  7645  unbnn  7682  fodomfi  7704  fival  7776  fiss  7788  dffi3  7795  hartogslem2  7871  card2on  7883  wdomima2g  7915  unxpwdom2  7917  unxpwdom  7918  harwdom  7919  oemapvali  8006  ackbij1lem11  8513  cofsmo  8552  ssfin4  8593  fin23lem11  8600  ssfin2  8603  ssfin3ds  8613  isfin1-3  8669  hsmex3  8717  axdc2lem  8731  ac6num  8762  zorn2lem1  8779  ttukeylem1  8792  ondomon  8841  fpwwe2lem3  8914  fpwwe2lem12  8922  fpwwe2lem13  8923  canthwe  8932  wuncss  9026  genpv  9282  genpdm  9285  hashss  12287  hashf1lem1  12329  wrdexg  12365  wrdexb  12366  shftfval  12680  o1of2  13211  o1rlimmul  13217  isercolllem2  13264  isstruct2  14304  ressabs  14358  prdsbas  14517  fnmrc  14667  mrcfval  14668  isacs1i  14717  mreacs  14718  isssc  14855  ipolerval  15448  ress0g  15572  symgbas  16007  sylow2a  16242  islbs3  17362  istps3OLD  18662  basdif0  18693  tgval  18695  eltg  18697  eltg2  18698  tgss  18708  basgen2  18729  2basgen  18730  tgdif0  18732  bastop1  18733  resttopon  18900  restabs  18904  restcld  18911  restfpw  18918  restcls  18920  restntr  18921  ordtbas2  18930  ordtbas  18931  lmfval  18971  cnrest  19024  cmpcov  19127  cmpsublem  19137  cmpsub  19138  2ndcomap  19197  txss12  19313  ptrescn  19347  trfbas2  19551  trfbas  19552  isfildlem  19565  snfbas  19574  trfil1  19594  trfil2  19595  trufil  19618  ssufl  19626  hauspwpwf1  19695  ustval  19912  psmetres2  20025  metrest  20234  cnheibor  20662  metcld2  20952  bcthlem1  20970  mbfimaopn2  21271  0pledm  21287  dvbss  21512  dvreslem  21520  dvres2lem  21521  dvcnp2  21530  dvaddbr  21548  dvmulbr  21549  dvcnvrelem2  21626  elply2  21800  plyf  21802  plyss  21803  elplyr  21805  plyeq0lem  21814  plyeq0  21815  plyaddlem  21819  plymullem  21820  dgrlem  21833  coeidlem  21841  ulmcn  22000  pserulm  22023  perpln1  23247  perpln2  23248  isperp  23249  iseupa  23758  issubgo  23962  rabexgfGS  26058  abrexdomjm  26060  dmct  26185  resf1o  26201  ress1r  26422  metidval  26482  indval  26635  sigagenss  26757  measval  26777  omsfval  26873  erdsze2lem1  27255  erdsze2lem2  27256  cvxpcon  27295  dfon2lem3  27762  setlikess  27820  altxpexg  28173  ivthALT  28698  islocfin  28736  filnetlem3  28769  abrexdom  28792  sdclem2  28806  sdclem1  28807  elrfirn  29199  pwssplit4  29610  hbtlem1  29647  hbtlem7  29649  rabexgf  29914  mpt2exxg2  30896  gsumlsscl  30989  lincellss  31112