Theorem ssexg 3917

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 3021	. . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵))
2	1	imbi1d 229	. . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)))
3		vex 2604	. . . 4 ⊢ 𝑥 ∈ V
4	3	ssex 3915	. . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V)
5	2, 4	vtoclg 2658	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))
6	5	impcom 123	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∧ wa 102   = wceq 1284   ∈ wcel 1433  Vcvv 2601   ⊆ wss 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-in 2979  df-ss 2986

This theorem is referenced by:  ssexd  3918  difexg  3919  rabexg  3921  elssabg  3923  elpw2g  3931  abssexg  3955  snexg  3956  sess1  4092  sess2  4093  trsuc  4177  unexb  4195  uniexb  4223  xpexg  4470  riinint  4611  dmexg  4614  rnexg  4615  resexg  4668  resiexg  4673  imaexg  4700  exse2  4719  cnvexg  4875  coexg  4882  fabexg  5097  f1oabexg  5158  relrnfvex  5213  fvexg  5214  sefvex  5216  mptfvex  5277  mptexg  5407  ofres  5745  resfunexgALT  5757  cofunexg  5758  fnexALT  5760  f1dmex  5763  oprabexd  5774  mpt2exxg  5853  tposexg  5896  frecabex  6007  erex  6153  ssdomg  6281  fiprc  6315  shftfvalg  9706  shftfval  9709