ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssexg GIF version

Theorem ssexg 4037
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.
StepHypRef Expression
1 sseq2 3091 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 230 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 2663 . . . 4 𝑥 ∈ V
43ssex 4035 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 2720 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 124 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1316  wcel 1465  Vcvv 2660  wss 3041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-in 3047  df-ss 3054
This theorem is referenced by:  ssexd  4038  difexg  4039  rabexg  4041  elssabg  4043  elpw2g  4051  abssexg  4076  snexg  4078  sess1  4229  sess2  4230  trsuc  4314  unexb  4333  abnexg  4337  uniexb  4364  xpexg  4623  riinint  4770  dmexg  4773  rnexg  4774  resexg  4829  resiexg  4834  imaexg  4863  exse2  4883  cnvexg  5046  coexg  5053  fabexg  5280  f1oabexg  5347  relrnfvex  5407  fvexg  5408  sefvex  5410  mptfvex  5474  mptexg  5613  ofres  5964  resfunexgALT  5976  cofunexg  5977  fnexALT  5979  f1dmex  5982  oprabexd  5993  mpoexxg  6076  tposexg  6123  frecabex  6263  erex  6421  mapex  6516  pmvalg  6521  elpmg  6526  elmapssres  6535  pmss12g  6537  ixpexgg  6584  ssdomg  6640  fiprc  6677  fival  6826  shftfvalg  10558  shftfval  10561  toponsspwpwg  12116  tgval  12145  tgvalex  12146  eltg  12148  eltg2  12149  tgss  12159  basgen2  12177  bastop1  12179  topnex  12182  resttopon  12267  restabs  12271  lmfval  12288  cnrest  12331  txss12  12362  metrest  12602  dvbss  12750  dvcnp2cntop  12759  dvaddxxbr  12761  dvmulxxbr  12762
  Copyright terms: Public domain W3C validator