Theorem ssexg 4172

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167  Vcvv 2763   ⊆ wss 3157

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-sep 4151

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170

This theorem is referenced by:  ssexd  4173  difexg  4174  rabexg  4176  elssabg  4181  elpw2g  4189  abssexg  4215  snexg  4217  sess1  4372  sess2  4373  trsuc  4457  unexb  4477  abnexg  4481  uniexb  4508  xpexg  4777  riinint  4927  dmexg  4930  rnexg  4931  resexg  4986  resiexg  4991  imaexg  5023  exse2  5043  cnvexg  5207  coexg  5214  fabexg  5445  f1oabexg  5516  relrnfvex  5576  fvexg  5577  sefvex  5579  mptfvex  5647  mptexg  5787  ofres  6150  resfunexgALT  6165  cofunexg  6166  fnexALT  6168  f1dmex  6173  oprabexd  6184  mpoexxg  6268  tposexg  6316  frecabex  6456  erex  6616  mapex  6713  pmvalg  6718  elpmg  6723  elmapssres  6732  pmss12g  6734  ixpexgg  6781  ssdomg  6837  fiprc  6874  fival  7036  iccen  10081  wrdexb  10947  shftfvalg  10983  shftfval  10986  tgval  12933  tgvalex  12934  toponsspwpwg  14258  eltg  14288  eltg2  14289  tgss  14299  basgen2  14317  bastop1  14319  topnex  14322  resttopon  14407  restabs  14411  lmfval  14428  cnrest  14471  txss12  14502  metrest  14742  dvbss  14921  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  elply2  14971  plyf  14973  plyss  14974  elplyr  14976  plyaddlem  14985  plymullem  14986  plyco  14995