New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  setswith Unicode version

Theorem setswith 4321
 Description: Two ways to express the class of all sets that contain . (Contributed by SF, 14-Jan-2015.)
Assertion
Ref Expression
setswith Sk k
Distinct variable group:   ,

Proof of Theorem setswith
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . . . 7
2 opkeq1 4059 . . . . . . . 8
32eleq1d 2419 . . . . . . 7 Sk Sk
41, 3rexsn 3768 . . . . . 6 Sk Sk
5 vex 2862 . . . . . . 7
6 elssetkg 4269 . . . . . . 7 Sk
75, 6mpan2 652 . . . . . 6 Sk
84, 7syl5rbb 249 . . . . 5 Sk
98abbidv 2467 . . . 4 Sk
10 df-imak 4189 . . . 4 Sk k Sk
119, 10syl6eqr 2403 . . 3 Sk k
12 iftrue 3668 . . 3 Sk k Sk k
1311, 12eqtr4d 2388 . 2 Sk k
14 elex 2867 . . . . . 6
1514con3i 127 . . . . 5
1615alrimiv 1631 . . . 4
17 ab0 3569 . . . 4
1816, 17sylibr 203 . . 3
19 iffalse 3669 . . 3 Sk k
2018, 19eqtr4d 2388 . 2 Sk k
2113, 20pm2.61i 156 1 Sk k
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 176  wal 1540   wceq 1642   wcel 1710  cab 2339  wrex 2615  cvv 2859  c0 3550  cif 3662  csn 3737  copk 4057  kcimak 4179   Sk cssetk 4183 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-if 3663  df-sn 3741  df-pr 3742  df-opk 4058  df-imak 4189  df-ssetk 4193 This theorem is referenced by:  setswithex  4322
 Copyright terms: Public domain W3C validator