Theorem ssexg 4128

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 3171	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 230	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 2733	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 4126	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 2790	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 124	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348   ∈ wcel 2141  Vcvv 2730   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-sep 4107

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134

This theorem is referenced by:  ssexd  4129  difexg  4130  rabexg  4132  elssabg  4134  elpw2g  4142  abssexg  4168  snexg  4170  sess1  4322  sess2  4323  trsuc  4407  unexb  4427  abnexg  4431  uniexb  4458  xpexg  4725  riinint  4872  dmexg  4875  rnexg  4876  resexg  4931  resiexg  4936  imaexg  4965  exse2  4985  cnvexg  5148  coexg  5155  fabexg  5385  f1oabexg  5454  relrnfvex  5514  fvexg  5515  sefvex  5517  mptfvex  5581  mptexg  5721  ofres  6075  resfunexgALT  6087  cofunexg  6088  fnexALT  6090  f1dmex  6095  oprabexd  6106  mpoexxg  6189  tposexg  6237  frecabex  6377  erex  6537  mapex  6632  pmvalg  6637  elpmg  6642  elmapssres  6651  pmss12g  6653  ixpexgg  6700  ssdomg  6756  fiprc  6793  fival  6947  iccen  9963  shftfvalg  10782  shftfval  10785  toponsspwpwg  12814  tgval  12843  tgvalex  12844  eltg  12846  eltg2  12847  tgss  12857  basgen2  12875  bastop1  12877  topnex  12880  resttopon  12965  restabs  12969  lmfval  12986  cnrest  13029  txss12  13060  metrest  13300  dvbss  13448  dvcnp2cntop  13457  dvaddxxbr  13459  dvmulxxbr  13460