Theorem ssexg 4254

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2205  Vcvv 2815   ⊆ wss 3214

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-sep 4233

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3220  df-ss 3227

This theorem is referenced by:  ssexd  4255  prcssprc  4256  difexg  4257  rabexg  4260  elssabg  4265  elpw2g  4273  abssexg  4300  snexg  4302  sess1  4463  sess2  4464  trsuc  4548  unexb  4568  abnexg  4572  uniexb  4599  xpexg  4869  riinint  5023  dmexg  5026  rnexg  5027  resexg  5083  resiexg  5088  imaexg  5120  exse2  5141  cnvexg  5305  coexg  5312  fabexg  5559  f1oabexg  5631  relrnfvex  5693  fvexg  5694  sefvex  5696  mptfvex  5768  mptexg  5916  ofres  6290  resfunexgALT  6310  cofunexg  6311  fnexALT  6313  f1dmex  6318  oprabexd  6333  mpoexxg  6419  suppfnss  6470  tposexg  6502  frecabex  6642  erex  6804  mapex  6901  pmvalg  6906  elpmg  6911  elmapssres  6920  pmss12g  6922  ixpexgg  6970  ssdomg  7031  fiprc  7070  fival  7270  iccen  10359  wrdexb  11261  shftfvalg  11528  shftfval  11531  tgval  13559  tgvalex  13560  toponsspwpwg  15013  eltg  15043  eltg2  15044  tgss  15054  basgen2  15072  bastop1  15074  topnex  15077  resttopon  15162  restabs  15166  lmfval  15184  cnrest  15226  txss12  15257  metrest  15497  dvbss  15676  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  elply2  15726  plyf  15728  plyss  15729  elplyr  15731  plyaddlem  15740  plymullem  15741  plyco  15750  clwwlkex  16519