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.

Step	Hyp	Ref	Expression
1		snex 4111	. . . . . . 7
2		opkeq1 4059	. . . . . . . 8
3	2	eleq1d 2419	. . . . . . 7 Sk Sk
4	1, 3	rexsn 3768	. . . . . 6 Sk Sk
5		vex 2862	. . . . . . 7
6		elssetkg 4269	. . . . . . 7 Sk
7	5, 6	mpan2 652	. . . . . 6 Sk
8	4, 7	syl5rbb 249	. . . . 5 Sk
9	8	abbidv 2467	. . . 4 Sk
10		df-imak 4189	. . . 4 Sk k Sk
11	9, 10	syl6eqr 2403	. . 3 Sk k
12		iftrue 3668	. . 3 Sk k Sk k
13	11, 12	eqtr4d 2388	. 2 Sk k
14		elex 2867	. . . . . 6
15	14	con3i 127	. . . . 5
16	15	alrimiv 1631	. . . 4
17		ab0 3569	. . . 4
18	16, 17	sylibr 203	. . 3
19		iffalse 3669	. . 3 Sk k
20	18, 19	eqtr4d 2388	. 2 Sk k
21	13, 20	pm2.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