P. 25 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-ne 2401	Define inequality. (Contributed by NM, 5-Aug-1993.)
|- ( A =/= B <-> -. A = B )
Theorem	neii 2402	Inference associated with df-ne 2401. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. A = B
Theorem	neir 2403	Inference associated with df-ne 2401. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- A =/= B
Theorem	nner 2404	Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( A = B -> -. A =/= B )
Theorem	nnedc 2405	Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( -. A =/= B <-> A = B ) )
Theorem	dcned 2406	Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
|- ( ph -> DECID A = B )   =>    |- ( ph -> DECID A =/= B )
Theorem	neqned 2407	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2421. One-way deduction form of df-ne 2401. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2450. (Revised by Wolf Lammen, 22-Nov-2019.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	neqne 2408	From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( -. A = B -> A =/= B )
Theorem	neirr 2409	No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- -. A =/= A
Theorem	eqneqall 2410	A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
|- ( A = B -> ( A =/= B -> ph ) )
Theorem	dcne 2411	Decidable equality expressed in terms of =/=. Basically the same as df-dc 840. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- (DECID A = B <-> ( A = B \/ A =/= B ) )
Theorem	nonconne 2412	Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
|- -. ( A = B /\ A =/= B )
Theorem	neeq1 2413	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2 2414	Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|- ( A = B -> ( C =/= A <-> C =/= B ) )
Theorem	neeq1i 2415	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( A =/= C <-> B =/= C )
Theorem	neeq2i 2416	Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|- A = B   =>    |- ( C =/= A <-> C =/= B )
Theorem	neeq12i 2417	Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|- A = B   &    |- C = D   =>    |- ( A =/= C <-> B =/= D )
Theorem	neeq1d 2418	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( A =/= C <-> B =/= C ) )
Theorem	neeq2d 2419	Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|- ( ph -> A = B )   =>    |- ( ph -> ( C =/= A <-> C =/= B ) )
Theorem	neeq12d 2420	Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> ( A =/= C <-> B =/= D ) )
Theorem	neneqd 2421	Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- ( ph -> A =/= B )   =>    |- ( ph -> -. A = B )
Theorem	neneq 2422	From inequality to non-equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A =/= B -> -. A = B )
Theorem	eqnetri 2423	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- B =/= C   =>    |- A =/= C
Theorem	eqnetrd 2424	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrri 2425	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A = B   &    |- A =/= C   =>    |- B =/= C
Theorem	eqnetrrd 2426	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= C )   =>    |- ( ph -> B =/= C )
Theorem	neeqtri 2427	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- B = C   =>    |- A =/= C
Theorem	neeqtrd 2428	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> B = C )   =>    |- ( ph -> A =/= C )
Theorem	neeqtrri 2429	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- A =/= B   &    |- C = B   =>    |- A =/= C
Theorem	neeqtrrd 2430	Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
|- ( ph -> A =/= B )   &    |- ( ph -> C = B )   =>    |- ( ph -> A =/= C )
Theorem	eqnetrrid 2431	B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
|- B = A   &    |- ( ph -> B =/= C )   =>    |- ( ph -> A =/= C )
Theorem	3netr3d 2432	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 2433	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 2434	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 2435	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 2436	Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
|- ( A = B <-> ph )   =>    |- ( A =/= B <-> -. ph )
Theorem	necon3bbii 2437	Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph <-> A = B )   =>    |- ( -. ph <-> A =/= B )
Theorem	necon3bii 2438	Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
|- ( A = B <-> C = D )   =>    |- ( A =/= B <-> C =/= D )
Theorem	necon3abid 2439	Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
|- ( ph -> ( A = B <-> ps ) )   =>    |- ( ph -> ( A =/= B <-> -. ps ) )
Theorem	necon3bbid 2440	Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
|- ( ph -> ( ps <-> A = B ) )   =>    |- ( ph -> ( -. ps <-> A =/= B ) )
Theorem	necon3bid 2441	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 2442	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> ( ps -> A = B ) )   =>    |- ( ph -> ( A =/= B -> -. ps ) )
Theorem	necon3bd 2443	Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> ( A = B -> ps ) )   =>    |- ( ph -> ( -. ps -> A =/= B ) )
Theorem	necon3d 2444	Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
|- ( ph -> ( A = B -> C = D ) )   =>    |- ( ph -> ( C =/= D -> A =/= B ) )
Theorem	nesym 2445	Characterization of inequality in terms of reversed equality (see bicom 140). (Contributed by BJ, 7-Jul-2018.)
|- ( A =/= B <-> -. B = A )
Theorem	nesymi 2446	Inference associated with nesym 2445. (Contributed by BJ, 7-Jul-2018.)
|- A =/= B   =>    |- -. B = A
Theorem	nesymir 2447	Inference associated with nesym 2445. (Contributed by BJ, 7-Jul-2018.)
|- -. A = B   =>    |- B =/= A
Theorem	necon3i 2448	Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
|- ( A = B -> C = D )   =>    |- ( C =/= D -> A =/= B )
Theorem	necon3ai 2449	Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( ph -> A = B )   =>    |- ( A =/= B -> -. ph )
Theorem	necon3bi 2450	Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|- ( A = B -> ph )   =>    |- ( -. ph -> A =/= B )
Theorem	necon1aidc 2451	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID ph -> ( -. ph -> A = B ) )   =>    |- (DECID ph -> ( A =/= B -> ph ) )
Theorem	necon1bidc 2452	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
|- (DECID A = B -> ( A =/= B -> ph ) )   =>    |- (DECID A = B -> ( -. ph -> A = B ) )
Theorem	necon1idc 2453	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( A =/= B -> C = D )   =>    |- (DECID A = B -> ( C =/= D -> A = B ) )
Theorem	necon2ai 2454	Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|- ( A = B -> -. ph )   =>    |- ( ph -> A =/= B )
Theorem	necon2bi 2455	Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
|- ( ph -> A =/= B )   =>    |- ( A = B -> -. ph )
Theorem	necon2i 2456	Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
|- ( A = B -> C =/= D )   =>    |- ( C = D -> A =/= B )
Theorem	necon2ad 2457	Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|- ( ph -> ( A = B -> -. ps ) )   =>    |- ( ph -> ( ps -> A =/= B ) )
Theorem	necon2bd 2458	Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
|- ( ph -> ( ps -> A =/= B ) )   =>    |- ( ph -> ( A = B -> -. ps ) )
Theorem	necon2d 2459	Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
|- ( ph -> ( A = B -> C =/= D ) )   =>    |- ( ph -> ( C = D -> A =/= B ) )
Theorem	necon1abiidc 2460	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( -. ph <-> A = B ) )   =>    |- (DECID ph -> ( A =/= B <-> ph ) )
Theorem	necon1bbiidc 2461	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B <-> ph ) )   =>    |- (DECID A = B -> ( -. ph <-> A = B ) )
Theorem	necon1abiddc 2462	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps <-> A = B ) ) )   =>    |- ( ph -> (DECID ps -> ( A =/= B <-> ps ) ) )
Theorem	necon1bbiddc 2463	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B <-> ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( -. ps <-> A = B ) ) )
Theorem	necon2abiidc 2464	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID ph -> ( A = B <-> -. ph ) )   =>    |- (DECID ph -> ( ph <-> A =/= B ) )
Theorem	necon2bbiidc 2465	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( ph <-> A =/= B ) )   =>    |- (DECID A = B -> ( A = B <-> -. ph ) )
Theorem	necon2abiddc 2466	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID ps -> ( A = B <-> -. ps ) ) )   =>    |- ( ph -> (DECID ps -> ( ps <-> A =/= B ) ) )
Theorem	necon2bbiddc 2467	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- ( ph -> (DECID A = B -> ( ps <-> A =/= B ) ) )   =>    |- ( ph -> (DECID A = B -> ( A = B <-> -. ps ) ) )
Theorem	necon4aidc 2468	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B -> -. ph ) )   =>    |- (DECID A = B -> ( ph -> A = B ) )
Theorem	necon4idc 2469	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
|- (DECID A = B -> ( A =/= B -> C =/= D ) )   =>    |- (DECID A = B -> ( C = D -> A = B ) )
Theorem	necon4addc 2470	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> -. ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( ps -> A = B ) ) )
Theorem	necon4bddc 2471	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps -> A =/= B ) ) )   =>    |- ( ph -> (DECID ps -> ( A = B -> ps ) ) )
Theorem	necon4ddc 2472	Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> C =/= D ) ) )   =>    |- ( ph -> (DECID A = B -> ( C = D -> A = B ) ) )
Theorem	necon4abiddc 2473	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
|- ( ph -> (DECID A = B -> (DECID ps -> ( A =/= B <-> -. ps ) ) ) )   =>    |- ( ph -> (DECID A = B -> (DECID ps -> ( A = B <-> ps ) ) ) )
Theorem	necon4bbiddc 2474	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID ps -> (DECID A = B -> ( -. ps <-> A =/= B ) ) ) )   =>    |- ( ph -> (DECID ps -> (DECID A = B -> ( ps <-> A = B ) ) ) )
Theorem	necon4biddc 2475	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> (DECID C = D -> ( A =/= B <-> C =/= D ) ) ) )   =>    |- ( ph -> (DECID A = B -> (DECID C = D -> ( A = B <-> C = D ) ) ) )
Theorem	necon1addc 2476	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID ps -> ( -. ps -> A = B ) ) )   =>    |- ( ph -> (DECID ps -> ( A =/= B -> ps ) ) )
Theorem	necon1bddc 2477	Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> ps ) ) )   =>    |- ( ph -> (DECID A = B -> ( -. ps -> A = B ) ) )
Theorem	necon1ddc 2478	Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- ( ph -> (DECID A = B -> ( A =/= B -> C = D ) ) )   =>    |- ( ph -> (DECID A = B -> ( C =/= D -> A = B ) ) )
Theorem	neneqad 2479	If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2421. One-way deduction form of df-ne 2401. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> -. A = B )   =>    |- ( ph -> A =/= B )
Theorem	nebidc 2480	Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
|- (DECID A = B -> (DECID C = D -> ( ( A = B <-> C = D ) <-> ( A =/= B <-> C =/= D ) ) ) )
Theorem	pm13.18 2481	Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ A =/= C ) -> B =/= C )
Theorem	pm13.181 2482	Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
|- ( ( A = B /\ B =/= C ) -> A =/= C )
Theorem	pm2.21ddne 2483	A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
|- ( ph -> A = B )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> ps )
Theorem	necom 2484	Commutation of inequality. (Contributed by NM, 14-May-1999.)
|- ( A =/= B <-> B =/= A )
Theorem	necomi 2485	Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
|- A =/= B   =>    |- B =/= A
Theorem	necomd 2486	Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
|- ( ph -> A =/= B )   =>    |- ( ph -> B =/= A )
Theorem	neanior 2487	A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|- ( ( A =/= B /\ C =/= D ) <-> -. ( A = B \/ C = D ) )
Theorem	ne3anior 2488	A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
|- ( ( A =/= B /\ C =/= D /\ E =/= F ) <-> -. ( A = B \/ C = D \/ E = F ) )
Theorem	nemtbir 2489	An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
|- A =/= B   &    |- ( ph <-> A = B )   =>    |- -. ph
Theorem	nelne1 2490	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 2491	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	nelelne 2492	Two classes are different if they don't belong to the same class. (Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV, 10-May-2020.)
|- ( -. A e. B -> ( C e. B -> C =/= A ) )
Theorem	nfne 2493	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 2494	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 )
2.1.4.2  Negated membership
Syntax	wnel 2495	Extend wff notation to include negated membership.
wff A e/ B
Definition	df-nel 2496	Define negated membership. (Contributed by NM, 7-Aug-1994.)
|- ( A e/ B <-> -. A e. B )
Theorem	neli 2497	Inference associated with df-nel 2496. (Contributed by BJ, 7-Jul-2018.)
|- A e/ B   =>    |- -. A e. B
Theorem	nelir 2498	Inference associated with df-nel 2496. (Contributed by BJ, 7-Jul-2018.)
|- -. A e. B   =>    |- A e/ B
Theorem	neleq1 2499	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( A e/ C <-> B e/ C ) )
Theorem	neleq2 2500	Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
|- ( A = B -> ( C e/ A <-> C e/ B ) )