Theorem ssexg 4571

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 3492	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 318	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 3090	. . . 4 |- x e. _V
4	3	ssex 4569	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3145	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 431	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 370   = wceq 1437   e. wcel 1870   _Vcvv 3087   C_ wss 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456

This theorem is referenced by:  ssexd  4572  difexg  4573  rabexg  4575  elssabg  4580  elpw2g  4588  abssexg  4610  snexALT  4611  sess1  4822  sess2  4823  riinint  5111  resexg  5167  trsuc  5526  ordsssuc2  5530  mptexg  6150  isofr2  6250  ofres  6561  brrpssg  6587  unexb  6605  xpexg  6607  difex2  6612  uniexb  6615  dmexg  6738  rnexg  6739  resiexg  6743  imaexg  6744  exse2  6746  cnvexg  6753  coexg  6758  fabexg  6763  f1oabexg  6766  resfunexgALT  6770  cofunexg  6771  fnexALT  6773  f1dmex  6777  oprabexd  6794  mpt2exxg  6881  suppfnss  6951  tposexg  6995  tz7.48-3  7169  oaabs  7353  erex  7395  mapex  7486  pmvalg  7491  elpmg  7495  elmapssres  7504  pmss12g  7506  ralxpmap  7529  ixpexg  7554  ssdomg  7622  fiprc  7658  domunsncan  7678  infensuc  7756  pssnn  7796  unbnn  7833  fodomfi  7856  fival  7932  fiss  7944  dffi3  7951  hartogslem2  8058  card2on  8069  wdomima2g  8101  unxpwdom2  8103  unxpwdom  8104  harwdom  8105  oemapvali  8188  ackbij1lem11  8658  cofsmo  8697  ssfin4  8738  fin23lem11  8745  ssfin2  8748  ssfin3ds  8758  isfin1-3  8814  hsmex3  8862  axdc2lem  8876  ac6num  8907  ttukeylem1  8937  ondomon  8986  fpwwe2lem3  9057  fpwwe2lem12  9065  fpwwe2lem13  9066  canthwe  9075  wuncss  9169  genpv  9423  genpdm  9426  hashss  12583  hashf1lem1  12613  wrdexg  12669  wrdexb  12670  shftfval  13112  o1of2  13654  o1rlimmul  13660  isercolllem2  13707  isstruct2  15093  ressval3d  15148  ressabs  15150  prdsbas  15314  fnmrc  15464  mrcfval  15465  isacs1i  15514  mreacs  15515  isssc  15676  ipolerval  16353  ress0g  16516  symgbas  16972  sylow2a  17206  islbs3  18313  basdif0  19899  tgval  19901  eltg  19903  eltg2  19904  tgss  19915  basgen2  19936  2basgen  19937  bastop1  19940  resttopon  20108  restabs  20112  restcld  20119  restfpw  20126  restcls  20128  restntr  20129  ordtbas2  20138  ordtbas  20139  lmfval  20179  cnrest  20232  cmpcov  20335  cmpsublem  20345  cmpsub  20346  2ndcomap  20404  islocfin  20463  txss12  20551  ptrescn  20585  trfbas2  20789  trfbas  20790  isfildlem  20803  snfbas  20812  trfil1  20832  trfil2  20833  trufil  20856  ssufl  20864  hauspwpwf1  20933  ustval  21148  metrest  21470  cnheibor  21879  metcld2  22169  bcthlem1  22185  mbfimaopn2  22490  0pledm  22508  dvbss  22733  dvreslem  22741  dvres2lem  22742  dvcnp2  22751  dvaddbr  22769  dvmulbr  22770  dvcnvrelem2  22847  elply2  23018  plyf  23020  plyss  23021  elplyr  23023  plyeq0lem  23032  plyeq0  23033  plyaddlem  23037  plymullem  23038  dgrlem  23051  coeidlem  23059  ulmcn  23219  pserulm  23242  iseupa  25538  issubgo  25876  rabexgfGS  27973  abrexdomjm  27977  mptexgf  28065  aciunf1  28105  dmct  28141  ress1r  28391  pcmplfin  28526  metidval  28532  indval  28674  sigagenss  28810  measval  28859  omsfval  28955  omssubaddlem  28960  omssubadd  28961  elcarsg  28966  carsggect  28979  carsgclctunlem3  28981  erdsze2lem1  29714  erdsze2lem2  29715  cvxpcon  29753  elmsta  29974  dfon2lem3  30218  altxpexg  30530  ivthALT  30776  filnetlem3  30821  abrexdom  31761  sdclem2  31775  sdclem1  31776  elrfirn  35246  pwssplit4  35653  hbtlem1  35688  hbtlem7  35690  rabexgf  36985  wessf1ornlem  37082  disjinfi  37091  dvnprodlem1  37390  dvnprodlem2  37391  sge0ss  37788  psmeasurelem  37817  caragensplit  37830  omeunile  37835  caragenuncl  37843  omeunle  37846  omeiunlempt  37850  carageniuncllem2  37852  mpt2exxg2  38879  gsumlsscl  38928  lincellss  38979