Theorem ssexg 4143

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  Vcvv 2738   ⊆ wss 3130

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4122

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-in 3136  df-ss 3143

This theorem is referenced by:  ssexd  4144  difexg  4145  rabexg  4147  elssabg  4149  elpw2g  4157  abssexg  4183  snexg  4185  sess1  4338  sess2  4339  trsuc  4423  unexb  4443  abnexg  4447  uniexb  4474  xpexg  4741  riinint  4889  dmexg  4892  rnexg  4893  resexg  4948  resiexg  4953  imaexg  4983  exse2  5003  cnvexg  5167  coexg  5174  fabexg  5404  f1oabexg  5474  relrnfvex  5534  fvexg  5535  sefvex  5537  mptfvex  5602  mptexg  5742  ofres  6097  resfunexgALT  6109  cofunexg  6110  fnexALT  6112  f1dmex  6117  oprabexd  6128  mpoexxg  6211  tposexg  6259  frecabex  6399  erex  6559  mapex  6654  pmvalg  6659  elpmg  6664  elmapssres  6673  pmss12g  6675  ixpexgg  6722  ssdomg  6778  fiprc  6815  fival  6969  iccen  10006  shftfvalg  10827  shftfval  10830  tgval  12711  tgvalex  12712  toponsspwpwg  13525  eltg  13555  eltg2  13556  tgss  13566  basgen2  13584  bastop1  13586  topnex  13589  resttopon  13674  restabs  13678  lmfval  13695  cnrest  13738  txss12  13769  metrest  14009  dvbss  14157  dvcnp2cntop  14166  dvaddxxbr  14168  dvmulxxbr  14169