Theorem ssexg 4199

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1373   ∈ wcel 2178  Vcvv 2776   ⊆ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180  df-ss 3187

This theorem is referenced by:  ssexd  4200  difexg  4201  rabexg  4203  elssabg  4208  elpw2g  4216  abssexg  4242  snexg  4244  sess1  4402  sess2  4403  trsuc  4487  unexb  4507  abnexg  4511  uniexb  4538  xpexg  4807  riinint  4958  dmexg  4961  rnexg  4962  resexg  5018  resiexg  5023  imaexg  5055  exse2  5075  cnvexg  5239  coexg  5246  fabexg  5485  f1oabexg  5556  relrnfvex  5617  fvexg  5618  sefvex  5620  mptfvex  5688  mptexg  5832  ofres  6196  resfunexgALT  6216  cofunexg  6217  fnexALT  6219  f1dmex  6224  oprabexd  6235  mpoexxg  6319  tposexg  6367  frecabex  6507  erex  6667  mapex  6764  pmvalg  6769  elpmg  6774  elmapssres  6783  pmss12g  6785  ixpexgg  6832  ssdomg  6893  fiprc  6931  fival  7098  iccen  10163  wrdexb  11043  shftfvalg  11244  shftfval  11247  tgval  13209  tgvalex  13210  toponsspwpwg  14609  eltg  14639  eltg2  14640  tgss  14650  basgen2  14668  bastop1  14670  topnex  14673  resttopon  14758  restabs  14762  lmfval  14779  cnrest  14822  txss12  14853  metrest  15093  dvbss  15272  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  elply2  15322  plyf  15324  plyss  15325  elplyr  15327  plyaddlem  15336  plymullem  15337  plyco  15346