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	nfcxfr 2601	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- F/_ x B   =>    |- F/_ x A
Theorem	nfcxfrd 2602	A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- A = B   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/_ x A )
Theorem	nfcv 2603*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x A
Theorem	nfcvd 2604*	If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )
Theorem	nfab1 2605	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/_ x { x | ph }
Theorem	nfnfc1 2606	x is bound in F/_ x A. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x F/_ x A
Theorem	nfab 2607	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/_ x { y | ph }
Theorem	nfaba1 2608	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
|- F/_ x { y | A. x ph }
Theorem	nfcrd 2609*	Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> F/_ x A )   =>    |- ( ph -> F/ x y e. A )
Theorem	nfeqd 2610	Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A = B )
Theorem	nfeld 2611	Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> F/_ x A )   &    |- ( ph -> F/_ x B )   =>    |- ( ph -> F/ x A e. B )
Theorem	nfnfc 2612	Hypothesis builder for F/_ y A. (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-13 2102. (Revised by Wolf Lammen, 10-Dec-2019.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfnfcALT 2613	Alternate proof of nfnfc 2612. Shorter but requiring more axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/_ x A   =>    |- F/ x F/_ y A
Theorem	nfeq 2614	Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A = B
Theorem	nfel 2615	Hypothesis builder for elementhood. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- F/ x A e. B
Theorem	nfeq1 2616*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A = B
Theorem	nfel1 2617*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x A   =>    |- F/ x A e. B
Theorem	nfeq2 2618*	Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A = B
Theorem	nfel2 2619*	Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
|- F/_ x B   =>    |- F/ x A e. B
Theorem	drnfc1 2620	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/_ x A <-> F/_ y B ) )
Theorem	drnfc2 2621	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/_ z A <-> F/_ z B ) )
Theorem	nfabd2 2622	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	nfabd 2623	Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/_ x { y | ps } )
Theorem	dvelimdc 2624	Deduction form of dvelimc 2625. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/_ x A )   &    |- ( ph -> F/_ z B )   &    |- ( ph -> ( z = y -> A = B ) )   =>    |- ( ph -> ( -. A. x x = y -> F/_ x B ) )
Theorem	dvelimc 2625	Version of dvelim 2182 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/_ x A   &    |- F/_ z B   &    |- ( z = y -> A = B )   =>    |- ( -. A. x x = y -> F/_ x B )
Theorem	nfcvf 2626	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/_ x y )
Theorem	nfcvf2 2627	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/_ y x )
Theorem	cleqf 2628	Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2563. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- F/_ x A   &    |- F/_ x B   =>    |- ( A = B <-> A. x ( x e. A <-> x e. B ) )
Theorem	abid2f 2629	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.) (Proof shortened by Wolf Lammen, 17-Nov-2019.)
|- F/_ x A   =>    |- { x | x e. A } = A
Theorem	abeq2f 2630	Equality of a class variable and a class abstraction. In this version, the fact that x is a non-free variable in A is explicitely stated as a hypothesis. (Contributed by Thierry Arnoux, 11-May-2017.)
|- F/_ x A   =>    |- ( A = { x | ph } <-> A. x ( x e. A <-> ph ) )
Theorem	sbabel 2631*	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.) (Proof shortened by Wolf Lammen, 26-Dec-2019.)
|- F/_ x A   =>    |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A )
Theorem	sbabelOLD 2632*	Obsolete proof of sbabel 2631 as of 26-Dec-2019. (Contributed by NM, 27-Sep-2003.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/_ x A   =>    |- ( [ y / x ] { z | ph } e. A <-> { z | [ y / x ] ph } e. A )
2.1.4  Negated equality and membership
Syntax	wne 2633	Extend wff notation to include inequality.
wff A =/= B
Syntax	wnel 2634	Extend wff notation to include negated membership.
wff A e/ B
Definition	df-ne 2635	Define inequality. (Contributed by NM, 26-May-1993.)
|- ( A =/= B <-> -. A = B )
Definition	df-nel 2636	Define negated membership. (Contributed by NM, 7-Aug-1994.)
|- ( A e/ B <-> -. A e. B )
2.1.4.1  Negated equality
Theorem	neii 2637	Inference associated with df-ne 2635. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2638	Inference associated with df-ne 2635. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nne 2639	Negation of inequality. (Contributed by NM, 9-Jun-2006.)
|- ( -. A =/= B <-> A = B )
Theorem	neneqd 2640	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neneq 2641	From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	neqned 2642	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2640. One-way deduction form of df-ne 2635. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2662. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neqne 2643	From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( -. A = B -> A =/= B )
Theorem	neirr 2644	No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
|- -. A =/= A
Theorem	exmidne 2645	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 2646	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	nonconne 2647	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 2648	Obsolete proof of nonconne 2647 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 2649	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 2650	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 2651	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 2652	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon1ad 2653	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 2654	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 2655	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 2656	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 2657	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	necon1d 2658	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 2659	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon4d 2660	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 2661	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 2662	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 2663	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 2664	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 2665	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 2666	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon4ai 2667	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 2668	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 2669	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A =/= B -> C = D )   =>    |- ( C =/= D -> A = B )
Theorem	necon2i 2670	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon4i 2671	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 2672	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- ( ph -> ( A = B <-> ps ) )   =>    |- ( ph -> ( A =/= B <-> -. ps ) )
Theorem	necon3bbid 2673	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon1abid 2674	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 2675	Contrapositive inference for inequality. (Contributed by NM, 31-Jan-2008.)
|- ( ph -> ( A =/= B <-> ps ) )   =>    |- ( ph -> ( -. ps <-> A = B ) )
Theorem	necon4abid 2676	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 2677	Contrapositive law deduction for inequality. (Contributed by NM, 9-May-2012.)
|- ( ph -> ( -. ps <-> A =/= B ) )   =>    |- ( ph -> ( ps <-> A = B ) )
Theorem	necon2abid 2678	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 2679	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 2680	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 2681	Contrapositive law deduction for inequality. (Contributed by NM, 29-Jun-2007.)
|- ( ph -> ( A =/= B <-> C =/= D ) )   =>    |- ( ph -> ( A = B <-> C = D ) )
Theorem	necon3abii 2682	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- ( A = B <-> ph )   =>    |- ( A =/= B <-> -. ph )
Theorem	necon3bbii 2683	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A = B )   =>    |- ( -. ph <-> A =/= B )
Theorem	necon1abii 2684	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 2685	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 2686	Contrapositive inference for inequality. (Contributed by NM, 2-Mar-2007.)
|- ( A = B <-> -. ph )   =>    |- ( ph <-> A =/= B )
Theorem	necon2bbii 2687	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A =/= B )   =>    |- ( A = B <-> -. ph )
Theorem	necon3bii 2688	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- ( A = B <-> C = D )   =>    |- ( A =/= B <-> C =/= D )
Theorem	necom 2689	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- ( A =/= B <-> B =/= A )
Theorem	necomi 2690	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>    |- B =/= A
Theorem	necomd 2691	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- ( ph -> A =/= B )   =>    |- ( ph -> B =/= A )
Theorem	nesym 2692	Characterization of inequality in terms of reversed equality (see bicom 205). (Contributed by BJ, 7-Jul-2018.)
|- ( A =/= B <-> -. B = A )
Theorem	nesymi 2693	Inference associated with nesym 2692. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- A =/= B   =>    |- -. B = A
Theorem	nesymir 2694	Inference associated with nesym 2692. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
|- -. A = B   =>    |- B =/= A
Theorem	neeq1d 2695	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 2696	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 2697	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 2698	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 2699	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 2700	Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )