Theorem ssexg 4168

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

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

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 4147

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 3159  df-ss 3166

This theorem is referenced by:  ssexd  4169  difexg  4170  rabexg  4172  elssabg  4177  elpw2g  4185  abssexg  4211  snexg  4213  sess1  4368  sess2  4369  trsuc  4453  unexb  4473  abnexg  4477  uniexb  4504  xpexg  4773  riinint  4923  dmexg  4926  rnexg  4927  resexg  4982  resiexg  4987  imaexg  5019  exse2  5039  cnvexg  5203  coexg  5210  fabexg  5441  f1oabexg  5512  relrnfvex  5572  fvexg  5573  sefvex  5575  mptfvex  5643  mptexg  5783  ofres  6145  resfunexgALT  6160  cofunexg  6161  fnexALT  6163  f1dmex  6168  oprabexd  6179  mpoexxg  6263  tposexg  6311  frecabex  6451  erex  6611  mapex  6708  pmvalg  6713  elpmg  6718  elmapssres  6727  pmss12g  6729  ixpexgg  6776  ssdomg  6832  fiprc  6869  fival  7029  iccen  10072  wrdexb  10926  shftfvalg  10962  shftfval  10965  tgval  12873  tgvalex  12874  toponsspwpwg  14190  eltg  14220  eltg2  14221  tgss  14231  basgen2  14249  bastop1  14251  topnex  14254  resttopon  14339  restabs  14343  lmfval  14360  cnrest  14403  txss12  14434  metrest  14674  dvbss  14839  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  elply2  14881  plyf  14883  plyss  14884  elplyr  14886  plyaddlem  14895  plymullem  14896