Theorem ssexg 3896

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 2967	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 220	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 2560	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 3894	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 2613	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 116	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1243   ∈ wcel 1393  Vcvv 2557   ⊆ wss 2917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-in 2924  df-ss 2931

This theorem is referenced by:  ssexd  3897  difexg  3898  rabexg  3900  elssabg  3902  elpw2g  3910  abssexg  3934  snexgOLD  3935  snexg  3936  sess1  4074  sess2  4075  trsuc  4159  unexb  4177  uniexb  4205  xpexg  4452  riinint  4593  dmexg  4596  rnexg  4597  resexg  4650  resiexg  4653  imaexg  4680  exse2  4699  cnvexg  4855  coexg  4862  fabexg  5077  f1oabexg  5138  relrnfvex  5193  fvexg  5194  sefvex  5196  mptfvex  5256  mptexg  5386  ofres  5725  resfunexgALT  5737  cofunexg  5738  fnexALT  5740  f1dmex  5743  oprabexd  5754  mpt2exxg  5833  tposexg  5873  frecabex  5984  erex  6130  ssdomg  6258  fiprc  6292  shftfvalg  9419  shftfval  9422