Theorem ssexg 4272

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ⊆ 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 4249

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  4273  prcssprc  4274  difexg  4275  rabexg  4279  elssabg  4284  elpw2g  4292  abssexg  4319  snexg  4321  sess1  4482  sess2  4483  trsuc  4567  unexb  4588  abnexg  4592  uniexb  4619  xpexg  4889  riinint  5043  dmexg  5046  rnexg  5047  resexg  5103  resiexg  5108  imaexg  5140  exse2  5161  cnvexg  5325  coexg  5332  fabexg  5579  f1oabexg  5651  relrnfvex  5713  fvexg  5714  sefvex  5716  mptfvex  5791  mptexg  5942  ofres  6317  resfunexgALT  6337  cofunexg  6338  fnexALT  6340  f1dmex  6345  oprabexd  6360  mpoexxg  6446  suppfnss  6497  tposexg  6529  frecabex  6669  erex  6831  mapex  6928  pmvalg  6933  elpmg  6938  elmapssres  6954  pmss12g  6956  ixpexgg  7004  ssdomg  7065  fiprc  7104  fival  7304  indval  9296  iccen  10409  wrdexb  11316  shftfvalg  11583  shftfval  11586  tgval  13616  tgvalex  13617  toponsspwpwg  15123  eltg  15153  eltg2  15154  tgss  15164  basgen2  15182  bastop1  15184  topnex  15187  resttopon  15272  restabs  15276  lmfval  15294  cnrest  15336  txss12  15367  metrest  15607  dvbss  15786  dvcnp2cntop  15800  dvaddxxbr  15802  dvmulxxbr  15803  elply2  15836  plyf  15838  plyss  15839  elplyr  15841  plyaddlem  15850  plymullem  15851  plyco  15860  clwwlkex  16639