Theorem ssexg 4139

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

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

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 4118

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 2739  df-in 3135  df-ss 3142

This theorem is referenced by:  ssexd  4140  difexg  4141  rabexg  4143  elssabg  4145  elpw2g  4153  abssexg  4179  snexg  4181  sess1  4334  sess2  4335  trsuc  4419  unexb  4439  abnexg  4443  uniexb  4470  xpexg  4737  riinint  4884  dmexg  4887  rnexg  4888  resexg  4943  resiexg  4948  imaexg  4978  exse2  4998  cnvexg  5162  coexg  5169  fabexg  5399  f1oabexg  5469  relrnfvex  5529  fvexg  5530  sefvex  5532  mptfvex  5597  mptexg  5737  ofres  6091  resfunexgALT  6103  cofunexg  6104  fnexALT  6106  f1dmex  6111  oprabexd  6122  mpoexxg  6205  tposexg  6253  frecabex  6393  erex  6553  mapex  6648  pmvalg  6653  elpmg  6658  elmapssres  6667  pmss12g  6669  ixpexgg  6716  ssdomg  6772  fiprc  6809  fival  6963  iccen  9990  shftfvalg  10808  shftfval  10811  toponsspwpwg  13180  tgval  13209  tgvalex  13210  eltg  13212  eltg2  13213  tgss  13223  basgen2  13241  bastop1  13243  topnex  13246  resttopon  13331  restabs  13335  lmfval  13352  cnrest  13395  txss12  13426  metrest  13666  dvbss  13814  dvcnp2cntop  13823  dvaddxxbr  13825  dvmulxxbr  13826