Theorem ssexg 4563

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 3466	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 323	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 3060	. . . 4 |- x e. _V
4	3	ssex 4561	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3119	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 436	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   e. wcel 1898   _Vcvv 3057   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430

This theorem is referenced by:  ssexd  4564  difexg  4565  rabexg  4567  elssabg  4572  elpw2g  4580  abssexg  4602  snexALT  4603  sess1  4821  sess2  4822  riinint  5110  resexg  5166  trsuc  5526  ordsssuc2  5530  mptexg  6160  isofr2  6260  ofres  6574  brrpssg  6600  unexb  6618  xpexg  6620  difex2  6625  uniexb  6628  dmexg  6751  rnexg  6752  resiexg  6756  imaexg  6757  exse2  6759  cnvexg  6766  coexg  6771  fabexg  6776  f1oabexg  6779  resfunexgALT  6783  cofunexg  6784  fnexALT  6786  f1dmex  6790  oprabexd  6807  mpt2exxg  6894  suppfnss  6967  tposexg  7013  tz7.48-3  7187  oaabs  7371  erex  7413  mapex  7504  pmvalg  7509  elpmg  7513  elmapssres  7522  pmss12g  7524  ralxpmap  7547  ixpexg  7572  ssdomg  7641  fiprc  7677  domunsncan  7698  infensuc  7776  pssnn  7816  unbnn  7853  fodomfi  7876  fival  7952  fiss  7964  dffi3  7971  hartogslem2  8084  card2on  8095  wdomima2g  8127  unxpwdom2  8129  unxpwdom  8130  harwdom  8131  oemapvali  8215  ackbij1lem11  8686  cofsmo  8725  ssfin4  8766  fin23lem11  8773  ssfin2  8776  ssfin3ds  8786  isfin1-3  8842  hsmex3  8890  axdc2lem  8904  ac6num  8935  ttukeylem1  8965  ondomon  9014  fpwwe2lem3  9084  fpwwe2lem12  9092  fpwwe2lem13  9093  canthwe  9102  wuncss  9196  genpv  9450  genpdm  9453  hashss  12618  hashf1lem1  12651  wrdexg  12715  wrdexb  12716  shftfval  13182  o1of2  13725  o1rlimmul  13731  isercolllem2  13778  isstruct2  15179  ressval3d  15235  ressabs  15237  prdsbas  15404  fnmrc  15562  mrcfval  15563  isacs1i  15612  mreacs  15613  isssc  15774  ipolerval  16451  ress0g  16614  symgbas  17070  sylow2a  17320  islbs3  18427  basdif0  20017  tgval  20019  eltg  20021  eltg2  20022  tgss  20033  basgen2  20054  2basgen  20055  bastop1  20058  resttopon  20226  restabs  20230  restcld  20237  restfpw  20244  restcls  20246  restntr  20247  ordtbas2  20256  ordtbas  20257  lmfval  20297  cnrest  20350  cmpcov  20453  cmpsublem  20463  cmpsub  20464  2ndcomap  20522  islocfin  20581  txss12  20669  ptrescn  20703  trfbas2  20907  trfbas  20908  isfildlem  20921  snfbas  20930  trfil1  20950  trfil2  20951  trufil  20974  ssufl  20982  hauspwpwf1  21051  ustval  21266  metrest  21588  cnheibor  22032  metcld2  22325  bcthlem1  22341  mbfimaopn2  22662  0pledm  22680  dvbss  22905  dvreslem  22913  dvres2lem  22914  dvcnp2  22923  dvaddbr  22941  dvmulbr  22942  dvcnvrelem2  23019  elply2  23199  plyf  23201  plyss  23202  elplyr  23204  plyeq0lem  23213  plyeq0  23214  plyaddlem  23218  plymullem  23219  dgrlem  23232  coeidlem  23240  ulmcn  23403  pserulm  23426  iseupa  25742  issubgo  26080  rabexgfGS  28186  abrexdomjm  28190  mptexgf  28274  aciunf1  28314  dmct  28347  ress1r  28601  pcmplfin  28736  metidval  28742  indval  28884  sigagenss  29020  measval  29069  omsfval  29167  omsfvalOLD  29171  omssubaddlem  29176  omssubadd  29177  omssubaddlemOLD  29180  omssubaddOLD  29181  elcarsg  29186  carsggect  29199  carsgclctunlem3  29201  erdsze2lem1  29975  erdsze2lem2  29976  cvxpcon  30014  elmsta  30235  dfon2lem3  30480  altxpexg  30794  ivthALT  31040  filnetlem3  31085  abrexdom  32102  sdclem2  32116  sdclem1  32117  elrfirn  35582  pwssplit4  35992  hbtlem1  36027  hbtlem7  36029  rabexgf  37385  wessf1ornlem  37497  disjinfi  37506  dvnprodlem1  37859  dvnprodlem2  37860  qndenserrnbllem  38201  sge0ss  38292  psmeasurelem  38346  caragensplit  38359  omeunile  38364  caragenuncl  38372  omeunle  38375  omeiunlempt  38379  carageniuncllem2  38381  prcssprc  39024  mpt2exxg2  40392  gsumlsscl  40441  lincellss  40492