Theorem ssexg 4249

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398   ∈ wcel 2203  Vcvv 2813   ⊆ wss 3211

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-sep 4228

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224

This theorem is referenced by:  ssexd  4250  prcssprc  4251  difexg  4252  rabexg  4255  elssabg  4260  elpw2g  4268  abssexg  4295  snexg  4297  sess1  4458  sess2  4459  trsuc  4543  unexb  4563  abnexg  4567  uniexb  4594  xpexg  4864  riinint  5018  dmexg  5021  rnexg  5022  resexg  5078  resiexg  5083  imaexg  5115  exse2  5136  cnvexg  5300  coexg  5307  fabexg  5554  f1oabexg  5626  relrnfvex  5688  fvexg  5689  sefvex  5691  mptfvex  5763  mptexg  5911  ofres  6281  resfunexgALT  6301  cofunexg  6302  fnexALT  6304  f1dmex  6309  oprabexd  6320  mpoexxg  6406  suppfnss  6457  tposexg  6489  frecabex  6629  erex  6791  mapex  6888  pmvalg  6893  elpmg  6898  elmapssres  6907  pmss12g  6909  ixpexgg  6957  ssdomg  7018  fiprc  7057  fival  7257  iccen  10340  wrdexb  11236  shftfvalg  11503  shftfval  11506  tgval  13475  tgvalex  13476  toponsspwpwg  14887  eltg  14917  eltg2  14918  tgss  14928  basgen2  14946  bastop1  14948  topnex  14951  resttopon  15036  restabs  15040  lmfval  15058  cnrest  15100  txss12  15131  metrest  15371  dvbss  15550  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  elply2  15600  plyf  15602  plyss  15603  elplyr  15605  plyaddlem  15614  plymullem  15615  plyco  15624  clwwlkex  16393