P. 26 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2501-2600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfel2 2501*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_xB   =>   |- F/x A e. B
Theorem	nfcrd 2502*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- (ph -> F/_xA)   =>   |- (ph -> F/x y e. A)
Theorem	nfeqd 2503	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/x A = B)
Theorem	nfeld 2504	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- (ph -> F/_xA)   &   |- (ph -> F/_xB)   =>   |- (ph -> F/x A e. B)
Theorem	drnfc1 2505	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- (A.x x = y -> A = B)   =>   |- (A.x x = y -> ( F/_xA <-> F/_yB))
Theorem	drnfc2 2506	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- (A.x x = y -> A = B)   =>   |- (A.x x = y -> ( F/_zA <-> F/_zB))
Theorem	nfabd2 2507	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/yph   &   |- ((ph /\ -. A.x x = y) -> F/xps)   =>   |- (ph -> F/_x{y | ps})
Theorem	nfabd 2508	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/_x{y | ps})
Theorem	dvelimdc 2509	Deduction form of dvelimc 2510. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/xph   &   |- F/zph   &   |- (ph -> F/_xA)   &   |- (ph -> F/_zB)   &   |- (ph -> (z = y -> A = B))   =>   |- (ph -> (-. A.x x = y -> F/_xB))
Theorem	dvelimc 2510	Version of dvelim 2016 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/_xA   &   |- F/_zB   &   |- (z = y -> A = B)   =>   |- (-. A.x x = y -> F/_xB)
Theorem	nfcvf 2511	If x and y are distinct, then x is not free in y. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- (-. A.x x = y -> F/_xy)
Theorem	nfcvf2 2512	If x and y are distinct, then y is not free in x. (Contributed by Mario Carneiro, 5-Dec-2016.)
|- (-. A.x x = y -> F/_yx)
Theorem	cleqf 2513	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   &   |- F/_xB   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
Theorem	abid2f 2514	A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 5-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   =>   |- {x | x e. A} = A
Theorem	sbabel 2515*	Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_xA   =>   |- ([y / x]{z | ph} e. A <-> {z | [y / x]ph} e. A)
2.1.4  Negated equality and membership
Syntax	wne 2516	Extend wff notation to include inequality.
wff A =/= B
Syntax	wnel 2517	Extend wff notation to include negated membership.
wff A e/ B
Definition	df-ne 2518	Define inequality. (Contributed by NM, 5-Aug-1993.)
|- (A =/= B <-> -. A = B)
Definition	df-nel 2519	Define negated membership. (Contributed by NM, 7-Aug-1994.)
|- (A e/ B <-> -. A e. B)
Theorem	nne 2520	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
|- (-. A =/= B <-> A = B)
Theorem	neirr 2521	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- -. A =/= A
Theorem	exmidne 2522	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- (A = B \/ A =/= B)
Theorem	nonconne 2523	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- -. (A = B /\ A =/= B)
Theorem	neeq1 2524	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- (A = B -> (A =/= C <-> B =/= C))
Theorem	neeq2 2525	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- (A = B -> (C =/= A <-> C =/= B))
Theorem	neeq1i 2526	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>   |- (A =/= C <-> B =/= C)
Theorem	neeq2i 2527	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>   |- (C =/= A <-> C =/= B)
Theorem	neeq12i 2528	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|- A = B   &   |- C = D   =>   |- (A =/= C <-> B =/= D)
Theorem	neeq1d 2529	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- (ph -> A = B)   =>   |- (ph -> (A =/= C <-> B =/= C))
Theorem	neeq2d 2530	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- (ph -> A = B)   =>   |- (ph -> (C =/= A <-> C =/= B))
Theorem	neeq12d 2531	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|- (ph -> A = B)   &   |- (ph -> C = D)   =>   |- (ph -> (A =/= C <-> B =/= D))
Theorem	neneqd 2532	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> A =/= B)   =>   |- (ph -> -. A = B)
Theorem	eqnetri 2533	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &   |- B =/= C   =>   |- A =/= C
Theorem	eqnetrd 2534	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- (ph -> A = B)   &   |- (ph -> B =/= C)   =>   |- (ph -> A =/= C)
Theorem	eqnetrri 2535	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &   |- A =/= C   =>   |- B =/= C
Theorem	eqnetrrd 2536	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- (ph -> A = B)   &   |- (ph -> A =/= C)   =>   |- (ph -> B =/= C)
Theorem	neeqtri 2537	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &   |- B = C   =>   |- A =/= C
Theorem	neeqtrd 2538	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- (ph -> A =/= B)   &   |- (ph -> B = C)   =>   |- (ph -> A =/= C)
Theorem	neeqtrri 2539	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &   |- C = B   =>   |- A =/= C
Theorem	neeqtrrd 2540	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- (ph -> A =/= B)   &   |- (ph -> C = B)   =>   |- (ph -> A =/= C)
Theorem	syl5eqner 2541	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
|- B = A   &   |- (ph -> B =/= C)   =>   |- (ph -> A =/= C)
Theorem	3netr3d 2542	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- (ph -> A =/= B)   &   |- (ph -> A = C)   &   |- (ph -> B = D)   =>   |- (ph -> C =/= D)
Theorem	3netr4d 2543	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- (ph -> A =/= B)   &   |- (ph -> C = A)   &   |- (ph -> D = B)   =>   |- (ph -> C =/= D)
Theorem	3netr3g 2544	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
|- (ph -> A =/= B)   &   |- A = C   &   |- B = D   =>   |- (ph -> C =/= D)
Theorem	3netr4g 2545	Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
|- (ph -> A =/= B)   &   |- C = A   &   |- D = B   =>   |- (ph -> C =/= D)
Theorem	necon3abii 2546	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- (A = B <-> ph)   =>   |- (A =/= B <-> -. ph)
Theorem	necon3bbii 2547	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- (ph <-> A = B)   =>   |- (-. ph <-> A =/= B)
Theorem	necon3bii 2548	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- (A = B <-> C = D)   =>   |- (A =/= B <-> C =/= D)
Theorem	necon3abid 2549	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- (ph -> (A = B <-> ps))   =>   |- (ph -> (A =/= B <-> -. ps))
Theorem	necon3bbid 2550	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- (ph -> (ps <-> A = B))   =>   |- (ph -> (-. ps <-> A =/= B))
Theorem	necon3bid 2551	Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A = B <-> C = D))   =>   |- (ph -> (A =/= B <-> C =/= D))
Theorem	necon3ad 2552	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (ps -> A = B))   =>   |- (ph -> (A =/= B -> -. ps))
Theorem	necon3bd 2553	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A = B -> ps))   =>   |- (ph -> (-. ps -> A =/= B))
Theorem	necon3d 2554	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- (ph -> (A = B -> C = D))   =>   |- (ph -> (C =/= D -> A =/= B))
Theorem	necon3i 2555	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
|- (A = B -> C = D)   =>   |- (C =/= D -> A =/= B)
Theorem	necon3ai 2556	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> A = B)   =>   |- (A =/= B -> -. ph)
Theorem	necon3bi 2557	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A = B -> ph)   =>   |- (-. ph -> A =/= B)
Theorem	necon1ai 2558	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.)
|- (-. ph -> A = B)   =>   |- (A =/= B -> ph)
Theorem	necon1bi 2559	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A =/= B -> ph)   =>   |- (-. ph -> A = B)
Theorem	necon1i 2560	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- (A =/= B -> C = D)   =>   |- (C =/= D -> A = B)
Theorem	necon2ai 2561	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A = B -> -. ph)   =>   |- (ph -> A =/= B)
Theorem	necon2bi 2562	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- (ph -> A =/= B)   =>   |- (A = B -> -. ph)
Theorem	necon2i 2563	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- (A = B -> C =/= D)   =>   |- (C = D -> A =/= B)
Theorem	necon2ad 2564	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A = B -> -. ps))   =>   |- (ph -> (ps -> A =/= B))
Theorem	necon2bd 2565	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- (ph -> (ps -> A =/= B))   =>   |- (ph -> (A = B -> -. ps))
Theorem	necon2d 2566	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- (ph -> (A = B -> C =/= D))   =>   |- (ph -> (C = D -> A =/= B))
Theorem	necon1abii 2567	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
|- (-. ph <-> A = B)   =>   |- (A =/= B <-> ph)
Theorem	necon1bbii 2568	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.)
|- (A =/= B <-> ph)   =>   |- (-. ph <-> A = B)
Theorem	necon1abid 2569	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.)
|- (ph -> (-. ps <-> A = B))   =>   |- (ph -> (A =/= B <-> ps))
Theorem	necon1bbid 2570	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
|- (ph -> (A =/= B <-> ps))   =>   |- (ph -> (-. ps <-> A = B))
Theorem	necon2abii 2571	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
|- (A = B <-> -. ph)   =>   |- (ph <-> A =/= B)
Theorem	necon2bbii 2572	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- (ph <-> A =/= B)   =>   |- (A = B <-> -. ph)
Theorem	necon2abid 2573	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.)
|- (ph -> (A = B <-> -. ps))   =>   |- (ph -> (ps <-> A =/= B))
Theorem	necon2bbid 2574	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.)
|- (ph -> (ps <-> A =/= B))   =>   |- (ph -> (A = B <-> -. ps))
Theorem	necon4ai 2575	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A =/= B -> -. ph)   =>   |- (ph -> A = B)
Theorem	necon4i 2576	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A =/= B -> C =/= D)   =>   |- (C = D -> A = B)
Theorem	necon4ad 2577	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A =/= B -> -. ps))   =>   |- (ph -> (ps -> A = B))
Theorem	necon4bd 2578	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (-. ps -> A =/= B))   =>   |- (ph -> (A = B -> ps))
Theorem	necon4d 2579	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A =/= B -> C =/= D))   =>   |- (ph -> (C = D -> A = B))
Theorem	necon4abid 2580	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.)
|- (ph -> (A =/= B <-> -. ps))   =>   |- (ph -> (A = B <-> ps))
Theorem	necon4bbid 2581	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
|- (ph -> (-. ps <-> A =/= B))   =>   |- (ph -> (ps <-> A = B))
Theorem	necon4bid 2582	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
|- (ph -> (A =/= B <-> C =/= D))   =>   |- (ph -> (A = B <-> C = D))
Theorem	necon1ad 2583	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.)
|- (ph -> (-. ps -> A = B))   =>   |- (ph -> (A =/= B -> ps))
Theorem	necon1bd 2584	Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A =/= B -> ps))   =>   |- (ph -> (-. ps -> A = B))
Theorem	necon1d 2585	Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A =/= B -> C = D))   =>   |- (ph -> (C =/= D -> A = B))
Theorem	neneqad 2586	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2532. One-way deduction form of df-ne 2518. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> -. A = B)   =>   |- (ph -> A =/= B)
Theorem	nebi 2587	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
|- ((A = B <-> C = D) <-> (A =/= B <-> C =/= D))
Theorem	pm13.18 2588	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ((A = B /\ A =/= C) -> B =/= C)
Theorem	pm13.181 2589	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ((A = B /\ B =/= C) -> A =/= C)
Theorem	pm2.21ddne 2590	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
|- (ph -> A = B)   &   |- (ph -> A =/= B)   =>   |- (ph -> ps)
Theorem	pm2.61ne 2591	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A = B -> (ps <-> ch))   &   |- ((ph /\ A =/= B) -> ps)   &   |- (ph -> ch)   =>   |- (ph -> ps)
Theorem	pm2.61ine 2592	Inference eliminating an inequality in an antecedent. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (A = B -> ph)   &   |- (A =/= B -> ph)   =>   |- ph
Theorem	pm2.61dne 2593	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- (ph -> (A = B -> ps))   &   |- (ph -> (A =/= B -> ps))   =>   |- (ph -> ps)
Theorem	pm2.61dane 2594	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
|- ((ph /\ A = B) -> ps)   &   |- ((ph /\ A =/= B) -> ps)   =>   |- (ph -> ps)
Theorem	pm2.61da2ne 2595	Deduction eliminating two inequalities in an antecedent. (Contributed by NM, 29-May-2013.)
|- ((ph /\ A = B) -> ps)   &   |- ((ph /\ C = D) -> ps)   &   |- ((ph /\ (A =/= B /\ C =/= D)) -> ps)   =>   |- (ph -> ps)
Theorem	pm2.61da3ne 2596	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.)
|- ((ph /\ A = B) -> ps)   &   |- ((ph /\ C = D) -> ps)   &   |- ((ph /\ E = F) -> ps)   &   |- ((ph /\ (A =/= B /\ C =/= D /\ E =/= F)) -> ps)   =>   |- (ph -> ps)
Theorem	necom 2597	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- (A =/= B <-> B =/= A)
Theorem	necomi 2598	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>   |- B =/= A
Theorem	necomd 2599	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- (ph -> A =/= B)   =>   |- (ph -> B =/= A)
Theorem	neor 2600	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
|- ((A = B \/ ps) <-> (A =/= B -> ps))