0nelsuc - New Foundations Explorer

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

Theorem 0nelsuc 4400

Description: The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
0nelsuc	1_c

Proof of Theorem 0nelsuc Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		el1c 4139	. . . . . . . . 9 1_c
2		vex 2862	. . . . . . . . . . . . 13
3	2	snid 3760	. . . . . . . . . . . 12
4		n0i 3555	. . . . . . . . . . . 12
5	3, 4	ax-mp 8	. . . . . . . . . . 11
6		eqeq1 2359	. . . . . . . . . . 11
7	5, 6	mtbiri 294	. . . . . . . . . 10
8	7	exlimiv 1634	. . . . . . . . 9
9	1, 8	sylbi 187	. . . . . . . 8 1_c
10		simpr 447	. . . . . . . 8 $/\$
11	9, 10	nsyl 113	. . . . . . 7 1_c $/\$
12		un00 3586	. . . . . . . . 9 $/\$
13		eqcom 2355	. . . . . . . . 9
14	12, 13	bitri 240	. . . . . . . 8 $/\$
15	14	notbii 287	. . . . . . 7 $/\$
16	11, 15	sylib 188	. . . . . 6 1_c
17		simpr 447	. . . . . 6 $/\$
18	16, 17	nsyl 113	. . . . 5 1_c $/\$
19	18	nrex 2716	. . . 4 1_c $/\$
20	19	a1i 10	. . 3 1_c $/\$
21	20	nrex 2716	. 2 1_c $/\$
22		eladdc 4398	. 2 1_c 1_c $/\$
23	21, 22	mtbir 290	1 1_c

Colors of variables: wff setvar class

Syntax hints:

wn 3 $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

wrex 2615

cun 3207

cin 3208

c0 3550

csn 3737 1_cc1c 4134

cplc 4375

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-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-ral 2619 df-rex 2620 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-ss 3259 df-nul 3551 df-sn 3741 df-1c 4136 df-addc 4378

This theorem is referenced by: 0cnsuc 4401 nndisjeq 4429 sfinltfin 4535