Theorem ssexg 4274

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  Vcvv 2821   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-sep 4251

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233

This theorem is used by:  ssexd  4275  prcssprc  4276  difexg  4277  rabexg  4281  elssabg  4286  elpw2g  4294  abssexg  4321  snexg  4323  sess1  4484  sess2  4485  trsuc  4569  unexb  4590  abnexg  4594  uniexb  4621  xpexg  4891  riinint  5045  dmexg  5048  rnexg  5049  resexg  5105  resiexg  5111  imaexg  5143  exse2  5164  cnvexg  5328  coexg  5335  fabexg  5582  f1oabexg  5654  relrnfvex  5716  fvexg  5717  sefvex  5719  mptfvex  5794  mptexg  5945  ofres  6321  resfunexgALT  6341  cofunexg  6342  fnexALT  6344  f1dmex  6349  oprabexd  6364  mpoexxg  6450  suppfnss  6501  tposexg  6534  frecabex  6674  erex  6836  mapex  6933  pmvalg  6938  elpmg  6943  elmapssres  6959  pmss12g  6961  ixpexgg  7010  ssdomg  7071  fiprc  7110  fival  7309  indval  9305  iccen  10425  wrdexb  11337  shftfvalg  11604  shftfval  11607  tgval  13674  tgvalex  13675  toponsspwpwg  15265  eltg  15295  eltg2  15296  tgss  15306  basgen2  15324  bastop1  15326  topnex  15329  resttopon  15414  restabs  15418  lmfval  15436  cnrest  15478  txss12  15509  metrest  15749  dvbss  15928  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  elply2  15978  plyf  15980  plyss  15981  elplyr  15983  plyaddlem  15992  plymullem  15993  plyco  16002  clwwlkex  16861