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

Theorem ssexg 4074
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 3125 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 230 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 2692 . . . 4 𝑥 ∈ V
43ssex 4072 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 2749 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 124 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1332  wcel 1481  Vcvv 2689  wss 3075
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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4053
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-in 3081  df-ss 3088
This theorem is referenced by:  ssexd  4075  difexg  4076  rabexg  4078  elssabg  4080  elpw2g  4088  abssexg  4113  snexg  4115  sess1  4266  sess2  4267  trsuc  4351  unexb  4370  abnexg  4374  uniexb  4401  xpexg  4660  riinint  4807  dmexg  4810  rnexg  4811  resexg  4866  resiexg  4871  imaexg  4900  exse2  4920  cnvexg  5083  coexg  5090  fabexg  5317  f1oabexg  5386  relrnfvex  5446  fvexg  5447  sefvex  5449  mptfvex  5513  mptexg  5652  ofres  6003  resfunexgALT  6015  cofunexg  6016  fnexALT  6018  f1dmex  6021  oprabexd  6032  mpoexxg  6115  tposexg  6162  frecabex  6302  erex  6460  mapex  6555  pmvalg  6560  elpmg  6565  elmapssres  6574  pmss12g  6576  ixpexgg  6623  ssdomg  6679  fiprc  6716  fival  6865  iccen  9818  shftfvalg  10621  shftfval  10624  toponsspwpwg  12226  tgval  12255  tgvalex  12256  eltg  12258  eltg2  12259  tgss  12269  basgen2  12287  bastop1  12289  topnex  12292  resttopon  12377  restabs  12381  lmfval  12398  cnrest  12441  txss12  12472  metrest  12712  dvbss  12860  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872
  Copyright terms: Public domain W3C validator