Theorem ssexg 4524

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 3452	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 315	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 3050	. . . 4 |- x e. _V
4	3	ssex 4522	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 3105	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 428	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399   e. wcel 1836   _Vcvv 3047   C_ wss 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-v 3049  df-in 3409  df-ss 3416

This theorem is referenced by:  ssexd  4525  difexg  4526  rabexg  4528  elssabg  4533  elpw2g  4541  abssexg  4563  snexALT  4564  sess1  4774  sess2  4775  trsuc  4889  ordsssuc2  4893  riinint  5185  resexg  5241  mptexg  6059  isofr2  6159  ofres  6472  brrpssg  6499  unexb  6517  xpexg  6519  difex2  6524  uniexb  6527  dmexg  6648  rnexg  6649  resiexg  6653  imaexg  6654  exse2  6656  cnvexg  6663  coexg  6668  fabexg  6673  f1oabexg  6676  resfunexgALT  6680  cofunexg  6681  fnexALT  6683  f1dmex  6687  oprabexd  6704  mpt2exxg  6791  suppfnss  6861  tposexg  6905  tz7.48-3  7045  oaabs  7229  erex  7271  mapex  7362  pmvalg  7367  elpmg  7371  elmapssres  7380  pmss12g  7382  ralxpmap  7405  ixpexg  7430  ssdomg  7498  fiprc  7534  domunsncan  7554  infensuc  7632  pssnn  7672  unbnn  7709  fodomfi  7732  fival  7805  fiss  7817  dffi3  7824  hartogslem2  7901  card2on  7913  wdomima2g  7945  unxpwdom2  7947  unxpwdom  7948  harwdom  7949  oemapvali  8034  ackbij1lem11  8541  cofsmo  8580  ssfin4  8621  fin23lem11  8628  ssfin2  8631  ssfin3ds  8641  isfin1-3  8697  hsmex3  8745  axdc2lem  8759  ac6num  8790  ttukeylem1  8820  ondomon  8869  fpwwe2lem3  8940  fpwwe2lem12  8948  fpwwe2lem13  8949  canthwe  8958  wuncss  9052  genpv  9306  genpdm  9309  hashss  12397  hashf1lem1  12427  wrdexg  12483  wrdexb  12484  shftfval  12924  o1of2  13456  o1rlimmul  13462  isercolllem2  13509  isstruct2  14662  ressval3d  14717  ressabs  14719  prdsbas  14883  fnmrc  15033  mrcfval  15034  isacs1i  15083  mreacs  15084  isssc  15245  ipolerval  15922  ress0g  16085  symgbas  16541  sylow2a  16775  islbs3  17933  istps3OLD  19527  basdif0  19558  tgval  19560  eltg  19562  eltg2  19563  tgss  19574  basgen2  19595  2basgen  19596  bastop1  19599  resttopon  19767  restabs  19771  restcld  19778  restfpw  19785  restcls  19787  restntr  19788  ordtbas2  19797  ordtbas  19798  lmfval  19838  cnrest  19891  cmpcov  19994  cmpsublem  20004  cmpsub  20005  2ndcomap  20063  islocfin  20122  txss12  20210  ptrescn  20244  trfbas2  20448  trfbas  20449  isfildlem  20462  snfbas  20471  trfil1  20491  trfil2  20492  trufil  20515  ssufl  20523  hauspwpwf1  20592  ustval  20809  metrest  21131  cnheibor  21559  metcld2  21849  bcthlem1  21867  mbfimaopn2  22168  0pledm  22184  dvbss  22409  dvreslem  22417  dvres2lem  22418  dvcnp2  22427  dvaddbr  22445  dvmulbr  22446  dvcnvrelem2  22523  elply2  22697  plyf  22699  plyss  22700  elplyr  22702  plyeq0lem  22711  plyeq0  22712  plyaddlem  22716  plymullem  22717  dgrlem  22730  coeidlem  22738  ulmcn  22898  pserulm  22921  iseupa  25107  issubgo  25443  rabexgfGS  27542  abrexdomjm  27546  mptexgf  27635  aciunf1  27679  dmct  27716  ress1r  27964  pcmplfin  28048  metidval  28054  indval  28193  sigagenss  28329  measval  28361  omsfval  28457  omssubaddlem  28462  omssubadd  28463  elcarsg  28468  carsggect  28481  carsgclctunlem3  28483  erdsze2lem1  28872  erdsze2lem2  28873  cvxpcon  28912  elmsta  29133  dfon2lem3  29418  setlikess  29476  altxpexg  29817  ivthALT  30355  filnetlem3  30400  abrexdom  30423  sdclem2  30437  sdclem1  30438  elrfirn  30829  pwssplit4  31237  hbtlem1  31276  hbtlem7  31278  rabexgf  31602  dvnprodlem1  31944  dvnprodlem2  31945  mpt2exxg2  33162  gsumlsscl  33211  lincellss  33262