Theorem ssexg 4228

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	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Proof of Theorem ssexg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 3251	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 231	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 2805	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4226	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 2864	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 125	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ wcel 2202  Vcvv 2802   ⊆ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-sep 4207

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-in 3206  df-ss 3213

This theorem is referenced by:  ssexd  4229  prcssprc  4230  difexg  4231  rabexg  4233  elssabg  4238  elpw2g  4246  abssexg  4272  snexg  4274  sess1  4434  sess2  4435  trsuc  4519  unexb  4539  abnexg  4543  uniexb  4570  xpexg  4840  riinint  4993  dmexg  4996  rnexg  4997  resexg  5053  resiexg  5058  imaexg  5090  exse2  5110  cnvexg  5274  coexg  5281  fabexg  5524  f1oabexg  5595  relrnfvex  5657  fvexg  5658  sefvex  5660  mptfvex  5732  mptexg  5878  ofres  6249  resfunexgALT  6269  cofunexg  6270  fnexALT  6272  f1dmex  6277  oprabexd  6288  mpoexxg  6374  tposexg  6423  frecabex  6563  erex  6725  mapex  6822  pmvalg  6827  elpmg  6832  elmapssres  6841  pmss12g  6843  ixpexgg  6890  ssdomg  6951  fiprc  6989  fival  7168  iccen  10240  wrdexb  11124  shftfvalg  11378  shftfval  11381  tgval  13344  tgvalex  13345  toponsspwpwg  14745  eltg  14775  eltg2  14776  tgss  14786  basgen2  14804  bastop1  14806  topnex  14809  resttopon  14894  restabs  14898  lmfval  14916  cnrest  14958  txss12  14989  metrest  15229  dvbss  15408  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  elply2  15458  plyf  15460  plyss  15461  elplyr  15463  plyaddlem  15472  plymullem  15473  plyco  15482  clwwlkex  16248