Theorem ssexg 4121

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1343   ∈ wcel 2136  Vcvv 2726   ⊆ wss 3116

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4100

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-in 3122  df-ss 3129

This theorem is referenced by:  ssexd  4122  difexg  4123  rabexg  4125  elssabg  4127  elpw2g  4135  abssexg  4161  snexg  4163  sess1  4315  sess2  4316  trsuc  4400  unexb  4420  abnexg  4424  uniexb  4451  xpexg  4718  riinint  4865  dmexg  4868  rnexg  4869  resexg  4924  resiexg  4929  imaexg  4958  exse2  4978  cnvexg  5141  coexg  5148  fabexg  5375  f1oabexg  5444  relrnfvex  5504  fvexg  5505  sefvex  5507  mptfvex  5571  mptexg  5710  ofres  6064  resfunexgALT  6076  cofunexg  6077  fnexALT  6079  f1dmex  6084  oprabexd  6095  mpoexxg  6178  tposexg  6226  frecabex  6366  erex  6525  mapex  6620  pmvalg  6625  elpmg  6630  elmapssres  6639  pmss12g  6641  ixpexgg  6688  ssdomg  6744  fiprc  6781  fival  6935  iccen  9942  shftfvalg  10760  shftfval  10763  toponsspwpwg  12660  tgval  12689  tgvalex  12690  eltg  12692  eltg2  12693  tgss  12703  basgen2  12721  bastop1  12723  topnex  12726  resttopon  12811  restabs  12815  lmfval  12832  cnrest  12875  txss12  12906  metrest  13146  dvbss  13294  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306