Type  Label  Description 
Statement 

Theorem  nfel2 2501* 
Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10Oct2016.)



Theorem  nfcrd 2502* 
Consequence of the notfree predicate. (Contributed by Mario Carneiro,
11Aug2016.)



Theorem  nfeqd 2503 
Hypothesis builder for equality. (Contributed by Mario Carneiro,
7Oct2016.)



Theorem  nfeld 2504 
Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
7Oct2016.)



Theorem  drnfc1 2505 
Formulabuilding lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  drnfc2 2506 
Formulabuilding lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  nfabd2 2507 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 8Oct2016.)



Theorem  nfabd 2508 
Boundvariable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 8Oct2016.)



Theorem  dvelimdc 2509 
Deduction form of dvelimc 2510. (Contributed by Mario Carneiro,
8Oct2016.)



Theorem  dvelimc 2510 
Version of dvelim 2016 for classes. (Contributed by Mario Carneiro,
8Oct2016.)



Theorem  nfcvf 2511 
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 8Oct2016.)



Theorem  nfcvf2 2512 
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 5Dec2016.)



Theorem  cleqf 2513 
Establish equality between classes, using boundvariable hypotheses
instead of distinct variable conditions. (Contributed by NM,
5Aug1993.) (Revised by Mario Carneiro, 7Oct2016.)



Theorem  abid2f 2514 
A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35.
(Contributed by NM, 5Sep2011.) (Revised by Mario Carneiro,
7Oct2016.)



Theorem  sbabel 2515* 
Theorem to move a substitution in and out of a class abstraction.
(Contributed by NM, 27Sep2003.) (Revised by Mario Carneiro,
7Oct2016.)



2.1.4 Negated equality and
membership


Syntax  wne 2516 
Extend wff notation to include inequality.



Syntax  wnel 2517 
Extend wff notation to include negated membership.



Definition  dfne 2518 
Define inequality. (Contributed by NM, 5Aug1993.)



Definition  dfnel 2519 
Define negated membership. (Contributed by NM, 7Aug1994.)



Theorem  nne 2520 
Negation of inequality. (Contributed by NM, 9Jun2006.)



Theorem  neirr 2521 
No class is unequal to itself. (Contributed by Stefan O'Rear,
1Jan2015.)



Theorem  exmidne 2522 
Excluded middle with equality and inequality. (Contributed by NM,
3Feb2012.)



Theorem  nonconne 2523 
Law of noncontradiction with equality and inequality. (Contributed by NM,
3Feb2012.)



Theorem  neeq1 2524 
Equality theorem for inequality. (Contributed by NM, 19Nov1994.)



Theorem  neeq2 2525 
Equality theorem for inequality. (Contributed by NM, 19Nov1994.)



Theorem  neeq1i 2526 
Inference for inequality. (Contributed by NM, 29Apr2005.)



Theorem  neeq2i 2527 
Inference for inequality. (Contributed by NM, 29Apr2005.)



Theorem  neeq12i 2528 
Inference for inequality. (Contributed by NM, 24Jul2012.)



Theorem  neeq1d 2529 
Deduction for inequality. (Contributed by NM, 25Oct1999.)



Theorem  neeq2d 2530 
Deduction for inequality. (Contributed by NM, 25Oct1999.)



Theorem  neeq12d 2531 
Deduction for inequality. (Contributed by NM, 24Jul2012.)



Theorem  neneqd 2532 
Deduction eliminating inequality definition. (Contributed by Jonathan
BenNaim, 3Jun2011.)



Theorem  eqnetri 2533 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrd 2534 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrri 2535 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  eqnetrrd 2536 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtri 2537 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrd 2538 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrri 2539 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  neeqtrrd 2540 
Substitution of equal classes into an inequality. (Contributed by NM,
4Jul2012.)



Theorem  syl5eqner 2541 
B chained equality inference for inequality. (Contributed by NM,
6Jun2012.)



Theorem  3netr3d 2542 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr4d 2543 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr3g 2544 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24Jul2012.)



Theorem  3netr4g 2545 
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14Jun2012.)



Theorem  necon3abii 2546 
Deduction from equality to inequality. (Contributed by NM,
9Nov2007.)



Theorem  necon3bbii 2547 
Deduction from equality to inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon3bii 2548 
Inference from equality to inequality. (Contributed by NM,
23Feb2005.)



Theorem  necon3abid 2549 
Deduction from equality to inequality. (Contributed by NM,
21Mar2007.)



Theorem  necon3bbid 2550 
Deduction from equality to inequality. (Contributed by NM,
2Jun2007.)



Theorem  necon3bid 2551 
Deduction from equality to inequality. (Contributed by NM,
23Feb2005.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon3ad 2552 
Contrapositive law deduction for inequality. (Contributed by NM,
2Apr2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon3bd 2553 
Contrapositive law deduction for inequality. (Contributed by NM,
2Apr2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon3d 2554 
Contrapositive law deduction for inequality. (Contributed by NM,
10Jun2006.)



Theorem  necon3i 2555 
Contrapositive inference for inequality. (Contributed by NM,
9Aug2006.)



Theorem  necon3ai 2556 
Contrapositive inference for inequality. (Contributed by NM,
23May2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon3bi 2557 
Contrapositive inference for inequality. (Contributed by NM,
1Jun2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon1ai 2558 
Contrapositive inference for inequality. (Contributed by NM,
12Feb2007.)



Theorem  necon1bi 2559 
Contrapositive inference for inequality. (Contributed by NM,
18Mar2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon1i 2560 
Contrapositive inference for inequality. (Contributed by NM,
18Mar2007.)



Theorem  necon2ai 2561 
Contrapositive inference for inequality. (Contributed by NM,
16Jan2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon2bi 2562 
Contrapositive inference for inequality. (Contributed by NM,
1Apr2007.)



Theorem  necon2i 2563 
Contrapositive inference for inequality. (Contributed by NM,
18Mar2007.)



Theorem  necon2ad 2564 
Contrapositive inference for inequality. (Contributed by NM,
19Apr2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon2bd 2565 
Contrapositive inference for inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon2d 2566 
Contrapositive inference for inequality. (Contributed by NM,
28Dec2008.)



Theorem  necon1abii 2567 
Contrapositive inference for inequality. (Contributed by NM,
17Mar2007.)



Theorem  necon1bbii 2568 
Contrapositive inference for inequality. (Contributed by NM,
17Mar2007.)



Theorem  necon1abid 2569 
Contrapositive deduction for inequality. (Contributed by NM,
21Aug2007.)



Theorem  necon1bbid 2570 
Contrapositive inference for inequality. (Contributed by NM,
31Jan2008.)



Theorem  necon2abii 2571 
Contrapositive inference for inequality. (Contributed by NM,
2Mar2007.)



Theorem  necon2bbii 2572 
Contrapositive inference for inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon2abid 2573 
Contrapositive deduction for inequality. (Contributed by NM,
18Jul2007.)



Theorem  necon2bbid 2574 
Contrapositive deduction for inequality. (Contributed by NM,
13Apr2007.)



Theorem  necon4ai 2575 
Contrapositive inference for inequality. (Contributed by NM,
16Jan2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon4i 2576 
Contrapositive inference for inequality. (Contributed by NM,
17Mar2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon4ad 2577 
Contrapositive inference for inequality. (Contributed by NM,
2Apr2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon4bd 2578 
Contrapositive inference for inequality. (Contributed by NM,
1Jun2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon4d 2579 
Contrapositive inference for inequality. (Contributed by NM,
2Apr2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon4abid 2580 
Contrapositive law deduction for inequality. (Contributed by NM,
11Jan2008.)



Theorem  necon4bbid 2581 
Contrapositive law deduction for inequality. (Contributed by NM,
9May2012.)



Theorem  necon4bid 2582 
Contrapositive law deduction for inequality. (Contributed by NM,
29Jun2007.)



Theorem  necon1ad 2583 
Contrapositive deduction for inequality. (Contributed by NM,
2Apr2007.)



Theorem  necon1bd 2584 
Contrapositive deduction for inequality. (Contributed by NM,
21Mar2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  necon1d 2585 
Contrapositive law deduction for inequality. (Contributed by NM,
28Dec2008.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  neneqad 2586 
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2532. Oneway deduction form of dfne 2518.
(Contributed by David Moews, 28Feb2017.)



Theorem  nebi 2587 
Contraposition law for inequality. (Contributed by NM, 28Dec2008.)



Theorem  pm13.18 2588 
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3Jun2011.)



Theorem  pm13.181 2589 
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3Jun2011.)



Theorem  pm2.21ddne 2590 
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28Feb2017.)



Theorem  pm2.61ne 2591 
Deduction eliminating an inequality in an antecedent. (Contributed by
NM, 24May2006.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  pm2.61ine 2592 
Inference eliminating an inequality in an antecedent. (Contributed by
NM, 16Jan2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  pm2.61dne 2593 
Deduction eliminating an inequality in an antecedent. (Contributed by
NM, 1Jun2007.) (Proof shortened by Andrew Salmon, 25May2011.)



Theorem  pm2.61dane 2594 
Deduction eliminating an inequality in an antecedent. (Contributed by
NM, 30Nov2011.)



Theorem  pm2.61da2ne 2595 
Deduction eliminating two inequalities in an antecedent. (Contributed
by NM, 29May2013.)



Theorem  pm2.61da3ne 2596 
Deduction eliminating three inequalities in an antecedent. (Contributed
by NM, 15Jun2013.)



Theorem  necom 2597 
Commutation of inequality. (Contributed by NM, 14May1999.)



Theorem  necomi 2598 
Inference from commutative law for inequality. (Contributed by NM,
17Oct2012.)



Theorem  necomd 2599 
Deduction from commutative law for inequality. (Contributed by NM,
12Feb2008.)



Theorem  neor 2600 
Logical OR with an equality. (Contributed by NM, 29Apr2007.)

