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  9299  iccen  10420  wrdexb  11331  shftfvalg  11598  shftfval  11601  tgval  13667  tgvalex  13668  toponsspwpwg  15175  eltg  15205  eltg2  15206  tgss  15216  basgen2  15234  bastop1  15236  topnex  15239  resttopon  15324  restabs  15328  lmfval  15346  cnrest  15388  txss12  15419  metrest  15659  dvbss  15838  dvcnp2cntop  15852  dvaddxxbr  15854  dvmulxxbr  15855  elply2  15888  plyf  15890  plyss  15891  elplyr  15893  plyaddlem  15902  plymullem  15903  plyco  15912  clwwlkex  16761