Theorem ssexg 4184

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2176  Vcvv 2772   ⊆ wss 3166

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-sep 4163

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179

This theorem is referenced by:  ssexd  4185  difexg  4186  rabexg  4188  elssabg  4193  elpw2g  4201  abssexg  4227  snexg  4229  sess1  4385  sess2  4386  trsuc  4470  unexb  4490  abnexg  4494  uniexb  4521  xpexg  4790  riinint  4940  dmexg  4943  rnexg  4944  resexg  5000  resiexg  5005  imaexg  5037  exse2  5057  cnvexg  5221  coexg  5228  fabexg  5465  f1oabexg  5536  relrnfvex  5596  fvexg  5597  sefvex  5599  mptfvex  5667  mptexg  5811  ofres  6175  resfunexgALT  6195  cofunexg  6196  fnexALT  6198  f1dmex  6203  oprabexd  6214  mpoexxg  6298  tposexg  6346  frecabex  6486  erex  6646  mapex  6743  pmvalg  6748  elpmg  6753  elmapssres  6762  pmss12g  6764  ixpexgg  6811  ssdomg  6872  fiprc  6909  fival  7074  iccen  10130  wrdexb  11008  shftfvalg  11162  shftfval  11165  tgval  13127  tgvalex  13128  toponsspwpwg  14527  eltg  14557  eltg2  14558  tgss  14568  basgen2  14586  bastop1  14588  topnex  14591  resttopon  14676  restabs  14680  lmfval  14697  cnrest  14740  txss12  14771  metrest  15011  dvbss  15190  dvcnp2cntop  15204  dvaddxxbr  15206  dvmulxxbr  15207  elply2  15240  plyf  15242  plyss  15243  elplyr  15245  plyaddlem  15254  plymullem  15255  plyco  15264