Theorem ssexg 4169

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2164  Vcvv 2760   ⊆ wss 3154

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-sep 4148

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160  df-ss 3167

This theorem is referenced by:  ssexd  4170  difexg  4171  rabexg  4173  elssabg  4178  elpw2g  4186  abssexg  4212  snexg  4214  sess1  4369  sess2  4370  trsuc  4454  unexb  4474  abnexg  4478  uniexb  4505  xpexg  4774  riinint  4924  dmexg  4927  rnexg  4928  resexg  4983  resiexg  4988  imaexg  5020  exse2  5040  cnvexg  5204  coexg  5211  fabexg  5442  f1oabexg  5513  relrnfvex  5573  fvexg  5574  sefvex  5576  mptfvex  5644  mptexg  5784  ofres  6147  resfunexgALT  6162  cofunexg  6163  fnexALT  6165  f1dmex  6170  oprabexd  6181  mpoexxg  6265  tposexg  6313  frecabex  6453  erex  6613  mapex  6710  pmvalg  6715  elpmg  6720  elmapssres  6729  pmss12g  6731  ixpexgg  6778  ssdomg  6834  fiprc  6871  fival  7031  iccen  10075  wrdexb  10929  shftfvalg  10965  shftfval  10968  tgval  12876  tgvalex  12877  toponsspwpwg  14201  eltg  14231  eltg2  14232  tgss  14242  basgen2  14260  bastop1  14262  topnex  14265  resttopon  14350  restabs  14354  lmfval  14371  cnrest  14414  txss12  14445  metrest  14685  dvbss  14864  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  elply2  14914  plyf  14916  plyss  14917  elplyr  14919  plyaddlem  14928  plymullem  14929  plyco  14937