P. 27 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2601-2700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	neneq 2601	From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	neqned 2602	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2600. One-way deduction form of df-ne 2595. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2621. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neirr 2603	No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- -. A =/= A
Theorem	exmidne 2604	Excluded middle with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- ( A = B \/ A =/= B )
Theorem	eqneqall 2605	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	nonconne 2606	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.) (Proof shortened by Wolf Lammen, 21-Dec-2019.)
|- -. ( A = B /\ A =/= B )
Theorem	nonconneOLD 2607	Obsolete proof of nonconne 2606 as of 21-Dec-2019. (Contributed by NM, 3-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
|- -. ( A = B /\ A =/= B )
Theorem	necon3ad 2608	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3bd 2609	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	necon2ad 2610	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2bd 2611	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon1ad 2612	Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( -. ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> ps ) )
Theorem	necon1bd 2613	Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A =/= B -> ps ) )   =>    |- ( ph -> ( -. ps -> A = B ) )
Theorem	necon4ad 2614	Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( A =/= B -> -. ps ) )   =>    |- ( ph -> ( ps -> A = B ) )
Theorem	necon4bd 2615	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
|- ( ph -> ( -. ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> ps ) )
Theorem	necon3d 2616	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	necon1d 2617	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	necon2d 2618	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon4d 2619	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	necon3ai 2620	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 2621	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon1ai 2622	Contrapositive inference for inequality. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( -. ph -> A = B )   =>    |- ( A =/= B -> ph )
Theorem	necon1bi 2623	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A =/= B -> ph )   =>    |- ( -. ph -> A = B )
Theorem	necon2ai 2624	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A = B -> -. ph )   =>    |- ( ph -> A =/= B )
Theorem	necon2bi 2625	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon4ai 2626	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A =/= B -> -. ph )   =>    |- ( ph -> A = B )
Theorem	necon3i 2627	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
|- ( A = B -> C = D )   =>    |- ( C =/= D -> A =/= B )
Theorem	necon1i 2628	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A =/= B -> C = D )   =>    |- ( C =/= D -> A = B )
Theorem	necon2i 2629	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon4i 2630	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( A =/= B -> C =/= D )   =>    |- ( C = D -> A = B )
Theorem	necon3abid 2631	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- ( ph -> ( A = B <-> ps ) )   =>    |- ( ph -> ( A =/= B <-> -. ps ) )
Theorem	necon3bbid 2632	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon1abid 2633	Contrapositive deduction for inequality. (Contributed by NM, 21-Aug-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( ph -> ( -. ps <-> A = B ) )   =>    |- ( ph -> ( A =/= B <-> ps ) )
Theorem	necon1bbid 2634	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
|- ( ph -> ( A =/= B <-> ps ) )   =>    |- ( ph -> ( -. ps <-> A = B ) )
Theorem	necon4abid 2635	Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( ph -> ( A =/= B <-> -. ps ) )   =>    |- ( ph -> ( A = B <-> ps ) )
Theorem	necon4bbid 2636	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
|- ( ph -> ( -. ps <-> A =/= B ) )   =>    |- ( ph -> ( ps <-> A = B ) )
Theorem	necon2abid 2637	Contrapositive deduction for inequality. (Contributed by NM, 18-Jul-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( ph -> ( A = B <-> -. ps ) )   =>    |- ( ph -> ( ps <-> A =/= B ) )
Theorem	necon2bbid 2638	Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( ph -> ( ps <-> A =/= B ) )   =>    |- ( ph -> ( A = B <-> -. ps ) )
Theorem	necon3bid 2639	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	necon4bid 2640	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
|- ( ph -> ( A =/= B <-> C =/= D ) )   =>    |- ( ph -> ( A = B <-> C = D ) )
Theorem	necon3abii 2641	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- ( A = B <-> ph )   =>    |- ( A =/= B <-> -. ph )
Theorem	necon3bbii 2642	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A = B )   =>    |- ( -. ph <-> A =/= B )
Theorem	necon1abii 2643	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( -. ph <-> A = B )   =>    |- ( A =/= B <-> ph )
Theorem	necon1bbii 2644	Contrapositive inference for inequality. (Contributed by NM, 17-Mar-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
|- ( A =/= B <-> ph )   =>    |- ( -. ph <-> A = B )
Theorem	necon2abii 2645	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
|- ( A = B <-> -. ph )   =>    |- ( ph <-> A =/= B )
Theorem	necon2bbii 2646	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A =/= B )   =>    |- ( A = B <-> -. ph )
Theorem	necon3bii 2647	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- ( A = B <-> C = D )   =>    |- ( A =/= B <-> C =/= D )
Theorem	necom 2648	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- ( A =/= B <-> B =/= A )
Theorem	necomi 2649	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>    |- B =/= A
Theorem	necomd 2650	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- ( ph -> A =/= B )   =>    |- ( ph -> B =/= A )
Theorem	nesym 2651	Characterization of inequality in terms of reversed equality (see bicom 203). (Contributed by BJ, 7-Jul-2018.)
|- ( A =/= B <-> -. B = A )
Theorem	nesymi 2652	Inference associated with nesym 2651. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- A =/= B   =>    |- -. B = A
Theorem	nesymir 2653	Inference associated with nesym 2651. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- -. A = B   =>    |- B =/= A
Theorem	neeq1d 2654	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2d 2655	Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C =/= A <-> C =/= B ) )
Theorem	neeq12d 2656	Deduction for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A =/= C <-> B =/= D ) )
Theorem	neeq1 2657	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
|- ( A = B -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2 2658	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)
|- ( A = B -> ( C =/= A <-> C =/= B ) )
Theorem	neeq1i 2659	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )
Theorem	neeq2i 2660	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- A = B   =>    |- ( C =/= A <-> C =/= B )
Theorem	neeq12i 2661	Inference for inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- A = B   &    |- C = D   =>    |- ( A =/= C <-> B =/= D )
Theorem	eqnetrd 2662	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrrd 2663	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> B =/= C )
Theorem	neeqtrd 2664	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetri 2665	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- B =/= C   =>    |- A =/= C
Theorem	eqnetrri 2666	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- A =/= C   =>    |- B =/= C
Theorem	neeqtri 2667	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- B = C   =>    |- A =/= C
Theorem	neeqtrri 2668	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- C = B   =>    |- A =/= C
Theorem	neeqtrrd 2669	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A =/= C )
Theorem	syl5eqner 2670	A chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- B = A   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	3netr3d 2671	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- ( ph -> A =/= B )   &    |- ( ph -> A = C )   &    |- ( ph -> B = D )   =>    |- ( ph -> C =/= D )
Theorem	3netr4d 2672	Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.) (Proof shortened by Wolf Lammen, 21-Nov-2019.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = A )   &    |- ( ph -> D = B )   =>    |- ( ph -> C =/= D )
Theorem	3netr3g 2673	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 2674	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	nebi 2675	Contraposition law for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ( A = B <-> C = D ) <-> ( A =/= B <-> C =/= D ) )
Theorem	pm13.18 2676	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ A =/= C ) -> B =/= C )
Theorem	pm13.181 2677	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ B =/= C ) -> A =/= C )
Theorem	pm2.61ine 2678	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.21ddne 2679	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 2680	Deduction eliminating an inequality in an antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( A = B -> ( ps <-> ch ) )   &    |- ( ( ph /\ A =/= B ) -> ps )   &    |- ( ph -> ch )   =>    |- ( ph -> ps )
Theorem	pm2.61dne 2681	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 2682	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 2683	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 2684	Deduction eliminating three inequalities in an antecedent. (Contributed by NM, 15-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( ( ph /\ A = B ) -> ps )   &    |- ( ( ph /\ C = D ) -> ps )   &    |- ( ( ph /\ E = F ) -> ps )   &    |- ( ( ph /\ ( A =/= B /\ C =/= D /\ E =/= F ) ) -> ps )   =>    |- ( ph -> ps )
Theorem	pm2.61iine 2685	Equality version of pm2.61ii 168. (Contributed by Scott Fenton, 13-Jun-2013.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( ( A =/= C /\ B =/= D ) -> ph )   &    |- ( A = C -> ph )   &    |- ( B = D -> ph )   =>    |- ph
Theorem	neor 2686	Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)
|- ( ( A = B \/ ps ) <-> ( A =/= B -> ps ) )
Theorem	neanior 2687	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B /\ C =/= D ) <-> -. ( A = B \/ C = D ) )
Theorem	ne3anior 2688	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
|- ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )
Theorem	neorian 2689	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B \/ C =/= D ) <-> -. ( A = B /\ C = D ) )
Theorem	nemtbir 2690	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
|- A =/= B   &    |- ( ph <-> A = B )   =>    |- -. ph
Theorem	nelne1 2691	Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
|- ( ( A e. B /\ -. A e. C ) -> B =/= C )
Theorem	nelne2 2692	Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
|- ( ( A e. C /\ -. B e. C ) -> A =/= B )
Theorem	neneor 2693	If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020.)
|- ( A =/= B -> ( A =/= C \/ B =/= C ) )
Theorem	nfne 2694	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A =/= B
Theorem	nfned 2695	Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A =/= B )
Theorem	nabbi 2696	Not equivalent wff's correspond to not equal class abstractions. (Contributed by AV, 7-Apr-2019.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( E. x ( ph <-> -. ps ) <-> { x | ph } =/= { x | ps } )
2.1.4.2  Negated membership
Theorem	neli 2697	Inference associated with df-nel 2596. (Contributed by BJ, 7-Jul-2018.)
|- A e/ B   =>    |- -. A e. B
Theorem	nelir 2698	Inference associated with df-nel 2596. (Contributed by BJ, 7-Jul-2018.)
|- -. A e. B   =>    |- A e/ B
Theorem	neleq12d 2699	Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A e/ C <-> B e/ D ) )
Theorem	neleq1 2700	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- ( A = B -> ( A e/ C <-> B e/ C ) )