Theorem ssexg 4007

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1299   ∈ wcel 1448  Vcvv 2641   ⊆ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-in 3027  df-ss 3034

This theorem is referenced by:  ssexd  4008  difexg  4009  rabexg  4011  elssabg  4013  elpw2g  4021  abssexg  4046  snexg  4048  sess1  4197  sess2  4198  trsuc  4282  unexb  4301  abnexg  4305  uniexb  4332  xpexg  4591  riinint  4736  dmexg  4739  rnexg  4740  resexg  4795  resiexg  4800  imaexg  4829  exse2  4849  cnvexg  5012  coexg  5019  fabexg  5246  f1oabexg  5313  relrnfvex  5371  fvexg  5372  sefvex  5374  mptfvex  5438  mptexg  5577  ofres  5927  resfunexgALT  5939  cofunexg  5940  fnexALT  5942  f1dmex  5945  oprabexd  5956  mpoexxg  6038  tposexg  6085  frecabex  6225  erex  6383  mapex  6478  pmvalg  6483  elpmg  6488  elmapssres  6497  pmss12g  6499  ixpexgg  6546  ssdomg  6602  fiprc  6639  shftfvalg  10431  shftfval  10434  toponsspwpwg  11971  tgval  12000  tgvalex  12001  eltg  12003  eltg2  12004  tgss  12014  basgen2  12032  bastop1  12034  topnex  12037  resttopon  12122  restabs  12126  lmfval  12143  cnrest  12185  txss12  12216  metrest  12434  dvbss  12527