Theorem ssexg 4274

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 3272	. . . 4 |- ( x = B -> ( A C_ x <-> A C_ B ) )
2	1	imbi1d 231	. . 3 |- ( x = B -> ( ( A C_ x -> A e. _V ) <-> ( A C_ B -> A e. _V ) ) )
3		vex 2824	. . . 4 |- x e. _V
4	3	ssex 4272	. . 3 |- ( A C_ x -> A e. _V )
5	2, 4	vtoclg 2883	. 2 |- ( B e. C -> ( A C_ B -> A e. _V ) )
6	5	impcom 125	1 |- ( ( A C_ B /\ B e. C ) -> A e. _V )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402   e. wcel 2209   _Vcvv 2821   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  ssexd  4275  prcssprc  4276  difexg  4277  rabexg  4281  elssabg  4286  elpw2g  4294  abssexg  4321  snexg  4323  sess1  4484  sess2  4485  trsuc  4569  unexb  4590  abnexg  4594  uniexb  4621  xpexg  4891  riinint  5045  dmexg  5048  rnexg  5049  resexg  5105  resiexg  5111  imaexg  5143  exse2  5164  cnvexg  5328  coexg  5335  fabexg  5582  f1oabexg  5654  relrnfvex  5716  fvexg  5717  sefvex  5719  mptfvex  5794  mptexg  5945  ofres  6321  resfunexgALT  6341  cofunexg  6342  fnexALT  6344  f1dmex  6349  oprabexd  6364  mpoexxg  6450  suppfnss  6501  tposexg  6533  frecabex  6673  erex  6835  mapex  6932  pmvalg  6937  elpmg  6942  elmapssres  6958  pmss12g  6960  ixpexgg  7008  ssdomg  7069  fiprc  7108  fival  7309  indval  9305  iccen  10426  wrdexb  11338  shftfvalg  11605  shftfval  11608  tgval  13675  tgvalex  13676  toponsspwpwg  15248  eltg  15278  eltg2  15279  tgss  15289  basgen2  15307  bastop1  15309  topnex  15312  resttopon  15397  restabs  15401  lmfval  15419  cnrest  15461  txss12  15492  metrest  15732  dvbss  15911  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  elply2  15961  plyf  15963  plyss  15964  elplyr  15966  plyaddlem  15975  plymullem  15976  plyco  15985  clwwlkex  16844