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

Theorem ssexg 3955
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 3037 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
21imbi1d 229 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥𝐴 ∈ V) ↔ (𝐴𝐵𝐴 ∈ V)))
3 vex 2618 . . . 4 𝑥 ∈ V
43ssex 3953 . . 3 (𝐴𝑥𝐴 ∈ V)
52, 4vtoclg 2672 . 2 (𝐵𝐶 → (𝐴𝐵𝐴 ∈ V))
65impcom 123 1 ((𝐴𝐵𝐵𝐶) → 𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1287  wcel 1436  Vcvv 2615  wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3934
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-in 2994  df-ss 3001
This theorem is referenced by:  ssexd  3956  difexg  3957  rabexg  3959  elssabg  3961  elpw2g  3969  abssexg  3993  snexg  3995  sess1  4140  sess2  4141  trsuc  4225  unexb  4243  uniexb  4271  xpexg  4522  riinint  4664  dmexg  4667  rnexg  4668  resexg  4721  resiexg  4726  imaexg  4755  exse2  4775  cnvexg  4936  coexg  4943  fabexg  5163  f1oabexg  5230  relrnfvex  5288  fvexg  5289  sefvex  5291  mptfvex  5353  mptexg  5485  ofres  5828  resfunexgALT  5840  cofunexg  5841  fnexALT  5843  f1dmex  5846  oprabexd  5857  mpt2exxg  5936  tposexg  5979  frecabex  6119  erex  6270  mapex  6365  pmvalg  6370  elpmg  6375  elmapssres  6384  pmss12g  6386  ssdomg  6449  fiprc  6486  shftfvalg  10152  shftfval  10155
  Copyright terms: Public domain W3C validator