necompl - New Foundations Explorer

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

Theorem necompl 3544

Description: A class is not equal to its complement. (Contributed by SF, 11-Jan-2015.)

**Assertion**
Ref	Expression
necompl	∼

Proof of Theorem necompl Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm5.19 349	. . . . 5
2		vex 2862	. . . . . . 7
3	2	elcompl 3225	. . . . . 6 ∼
4	3	bibi2i 304	. . . . 5 ∼
5	1, 4	mtbir 290	. . . 4 ∼
6		19.8a 1756	. . . 4 ∼ ∼
7	5, 6	ax-mp 8	. . 3 ∼
8		dfcleq 2347	. . . . 5 ∼ ∼
9	8	necon3abii 2546	. . . 4 ∼ ∼
10		exnal 1574	. . . 4 ∼ ∼
11	9, 10	bitr4i 243	. . 3 ∼ ∼
12	7, 11	mpbir 200	. 2 ∼
13	12	necomi 2598	1 ∼

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176

wal 1540

wex 1541

wcel 1710

wne 2516 ∼ ccompl 3205

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

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-v 2861 df-nin 3211 df-compl 3212

This theorem is referenced by: nfunv 5138 endisj 6051 ncaddccl 6144 tcdi 6164