Theorem ssexg 4226

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  Vcvv 2800   ⊆ wss 3198

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-sep 4205

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-in 3204  df-ss 3211

This theorem is referenced by:  ssexd  4227  prcssprc  4228  difexg  4229  rabexg  4231  elssabg  4236  elpw2g  4244  abssexg  4270  snexg  4272  sess1  4432  sess2  4433  trsuc  4517  unexb  4537  abnexg  4541  uniexb  4568  xpexg  4838  riinint  4991  dmexg  4994  rnexg  4995  resexg  5051  resiexg  5056  imaexg  5088  exse2  5108  cnvexg  5272  coexg  5279  fabexg  5521  f1oabexg  5592  relrnfvex  5653  fvexg  5654  sefvex  5656  mptfvex  5728  mptexg  5874  ofres  6245  resfunexgALT  6265  cofunexg  6266  fnexALT  6268  f1dmex  6273  oprabexd  6284  mpoexxg  6370  tposexg  6419  frecabex  6559  erex  6721  mapex  6818  pmvalg  6823  elpmg  6828  elmapssres  6837  pmss12g  6839  ixpexgg  6886  ssdomg  6947  fiprc  6985  fival  7160  iccen  10231  wrdexb  11115  shftfvalg  11369  shftfval  11372  tgval  13335  tgvalex  13336  toponsspwpwg  14736  eltg  14766  eltg2  14767  tgss  14777  basgen2  14795  bastop1  14797  topnex  14800  resttopon  14885  restabs  14889  lmfval  14907  cnrest  14949  txss12  14980  metrest  15220  dvbss  15399  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  elply2  15449  plyf  15451  plyss  15452  elplyr  15454  plyaddlem  15463  plymullem  15464  plyco  15473  clwwlkex  16193