Theorem ssexg 4508

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 3424	. . . 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 3020	. . . 4 |- x e. _V
4	3	ssex 4506	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3077	. 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 1872   _Vcvv 3017   C_ wss 3374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381  df-ss 3388

This theorem is referenced by:  ssexd  4509  difexg  4510  rabexg  4512  elssabg  4517  elpw2g  4525  abssexg  4547  snexALT  4548  sess1  4759  sess2  4760  riinint  5048  resexg  5104  trsuc  5464  ordsssuc2  5468  mptexg  6089  isofr2  6189  ofres  6500  brrpssg  6526  unexb  6544  xpexg  6546  difex2  6551  uniexb  6554  dmexg  6677  rnexg  6678  resiexg  6682  imaexg  6683  exse2  6685  cnvexg  6692  coexg  6697  fabexg  6702  f1oabexg  6705  resfunexgALT  6709  cofunexg  6710  fnexALT  6712  f1dmex  6716  oprabexd  6733  mpt2exxg  6820  suppfnss  6890  tposexg  6937  tz7.48-3  7111  oaabs  7295  erex  7337  mapex  7428  pmvalg  7433  elpmg  7437  elmapssres  7446  pmss12g  7448  ralxpmap  7471  ixpexg  7496  ssdomg  7564  fiprc  7600  domunsncan  7620  infensuc  7698  pssnn  7738  unbnn  7775  fodomfi  7798  fival  7874  fiss  7886  dffi3  7893  hartogslem2  8006  card2on  8017  wdomima2g  8049  unxpwdom2  8051  unxpwdom  8052  harwdom  8053  oemapvali  8136  ackbij1lem11  8606  cofsmo  8645  ssfin4  8686  fin23lem11  8693  ssfin2  8696  ssfin3ds  8706  isfin1-3  8762  hsmex3  8810  axdc2lem  8824  ac6num  8855  ttukeylem1  8885  ondomon  8934  fpwwe2lem3  9004  fpwwe2lem12  9012  fpwwe2lem13  9013  canthwe  9022  wuncss  9116  genpv  9370  genpdm  9373  hashss  12531  hashf1lem1  12561  wrdexg  12625  wrdexb  12626  shftfval  13072  o1of2  13614  o1rlimmul  13620  isercolllem2  13667  isstruct2  15068  ressval3d  15124  ressabs  15126  prdsbas  15293  fnmrc  15451  mrcfval  15452  isacs1i  15501  mreacs  15502  isssc  15663  ipolerval  16340  ress0g  16503  symgbas  16959  sylow2a  17209  islbs3  18316  basdif0  19905  tgval  19907  eltg  19909  eltg2  19910  tgss  19921  basgen2  19942  2basgen  19943  bastop1  19946  resttopon  20114  restabs  20118  restcld  20125  restfpw  20132  restcls  20134  restntr  20135  ordtbas2  20144  ordtbas  20145  lmfval  20185  cnrest  20238  cmpcov  20341  cmpsublem  20351  cmpsub  20352  2ndcomap  20410  islocfin  20469  txss12  20557  ptrescn  20591  trfbas2  20795  trfbas  20796  isfildlem  20809  snfbas  20818  trfil1  20838  trfil2  20839  trufil  20862  ssufl  20870  hauspwpwf1  20939  ustval  21154  metrest  21476  cnheibor  21920  metcld2  22213  bcthlem1  22229  mbfimaopn2  22550  0pledm  22568  dvbss  22793  dvreslem  22801  dvres2lem  22802  dvcnp2  22811  dvaddbr  22829  dvmulbr  22830  dvcnvrelem2  22907  elply2  23087  plyf  23089  plyss  23090  elplyr  23092  plyeq0lem  23101  plyeq0  23102  plyaddlem  23106  plymullem  23107  dgrlem  23120  coeidlem  23128  ulmcn  23291  pserulm  23314  iseupa  25630  issubgo  25968  rabexgfGS  28075  abrexdomjm  28079  mptexgf  28166  aciunf1  28206  dmct  28243  ress1r  28499  pcmplfin  28634  metidval  28640  indval  28782  sigagenss  28918  measval  28967  omsfval  29065  omsfvalOLD  29069  omssubaddlem  29074  omssubadd  29075  omssubaddlemOLD  29078  omssubaddOLD  29079  elcarsg  29084  carsggect  29097  carsgclctunlem3  29099  erdsze2lem1  29873  erdsze2lem2  29874  cvxpcon  29912  elmsta  30133  dfon2lem3  30377  altxpexg  30689  ivthALT  30935  filnetlem3  30980  abrexdom  31964  sdclem2  31978  sdclem1  31979  elrfirn  35449  pwssplit4  35860  hbtlem1  35895  hbtlem7  35897  rabexgf  37261  wessf1ornlem  37363  disjinfi  37372  dvnprodlem1  37704  dvnprodlem2  37705  sge0ss  38105  psmeasurelem  38159  caragensplit  38172  omeunile  38177  caragenuncl  38185  omeunle  38188  omeiunlempt  38192  carageniuncllem2  38194  mpt2exxg2  39712  gsumlsscl  39761  lincellss  39812