Theorem ssexg 4223

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 3248	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 231	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 2802	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4221	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 2861	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 125	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  Vcvv 2799   ⊆ wss 3197

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4202

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210

This theorem is referenced by:  ssexd  4224  prcssprc  4225  difexg  4226  rabexg  4228  elssabg  4233  elpw2g  4241  abssexg  4267  snexg  4269  sess1  4429  sess2  4430  trsuc  4514  unexb  4534  abnexg  4538  uniexb  4565  xpexg  4835  riinint  4988  dmexg  4991  rnexg  4992  resexg  5048  resiexg  5053  imaexg  5085  exse2  5105  cnvexg  5269  coexg  5276  fabexg  5518  f1oabexg  5589  relrnfvex  5650  fvexg  5651  sefvex  5653  mptfvex  5725  mptexg  5871  ofres  6242  resfunexgALT  6262  cofunexg  6263  fnexALT  6265  f1dmex  6270  oprabexd  6281  mpoexxg  6367  tposexg  6415  frecabex  6555  erex  6717  mapex  6814  pmvalg  6819  elpmg  6824  elmapssres  6833  pmss12g  6835  ixpexgg  6882  ssdomg  6943  fiprc  6981  fival  7153  iccen  10219  wrdexb  11101  shftfvalg  11350  shftfval  11353  tgval  13316  tgvalex  13317  toponsspwpwg  14717  eltg  14747  eltg2  14748  tgss  14758  basgen2  14776  bastop1  14778  topnex  14781  resttopon  14866  restabs  14870  lmfval  14888  cnrest  14930  txss12  14961  metrest  15201  dvbss  15380  dvcnp2cntop  15394  dvaddxxbr  15396  dvmulxxbr  15397  elply2  15430  plyf  15432  plyss  15433  elplyr  15435  plyaddlem  15444  plymullem  15445  plyco  15454  clwwlkex  16167