Theorem List for Intuitionistic Logic Explorer - 2301-2400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nfcvf 2301 |
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 8-Oct-2016.)
|
|
|
Theorem | nfcvf2 2302 |
If and are distinct, then is not free in .
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
|
|
Theorem | cleqf 2303 |
Establish equality between classes, using bound-variable hypotheses
instead of distinct variable conditions. See also cleqh 2237.
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
|
|
Theorem | abid2f 2304 |
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.)
|
|
|
Theorem | sbabel 2305* |
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.)
|
|
|
2.1.4 Negated equality and
membership
|
|
2.1.4.1 Negated equality
|
|
Syntax | wne 2306 |
Extend wff notation to include inequality.
|
|
|
Definition | df-ne 2307 |
Define inequality. (Contributed by NM, 5-Aug-1993.)
|
|
|
Theorem | neii 2308 |
Inference associated with df-ne 2307. (Contributed by BJ, 7-Jul-2018.)
|
|
|
Theorem | neir 2309 |
Inference associated with df-ne 2307. (Contributed by BJ, 7-Jul-2018.)
|
|
|
Theorem | nner 2310 |
Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|
|
|
Theorem | nnedc 2311 |
Negation of inequality where equality is decidable. (Contributed by Jim
Kingdon, 15-May-2018.)
|
DECID |
|
Theorem | dcned 2312 |
Decidable equality implies decidable negated equality. (Contributed by
Jim Kingdon, 3-May-2020.)
|
DECID
DECID
|
|
Theorem | neqned 2313 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2327. One-way deduction form of df-ne 2307.
(Contributed by David Moews, 28-Feb-2017.) Allow a shortening of
necon3bi 2356. (Revised by Wolf Lammen, 22-Nov-2019.)
|
|
|
Theorem | neqne 2314 |
From non-equality to inequality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | neirr 2315 |
No class is unequal to itself. (Contributed by Stefan O'Rear,
1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
|
|
Theorem | eqneqall 2316 |
A contradiction concerning equality implies anything. (Contributed by
Alexander van der Vekens, 25-Jan-2018.)
|
|
|
Theorem | dcne 2317 |
Decidable equality expressed in terms of . Basically the same as
df-dc 820. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
DECID |
|
Theorem | nonconne 2318 |
Law of noncontradiction with equality and inequality. (Contributed by NM,
3-Feb-2012.)
|
|
|
Theorem | neeq1 2319 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
|
|
Theorem | neeq2 2320 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
|
|
Theorem | neeq1i 2321 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
|
|
Theorem | neeq2i 2322 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
|
|
Theorem | neeq12i 2323 |
Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|
|
|
Theorem | neeq1d 2324 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
|
|
Theorem | neeq2d 2325 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
|
|
Theorem | neeq12d 2326 |
Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|
|
|
Theorem | neneqd 2327 |
Deduction eliminating inequality definition. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
|
|
Theorem | neneq 2328 |
From inequality to non-equality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
|
|
Theorem | eqnetri 2329 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | eqnetrd 2330 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | eqnetrri 2331 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | eqnetrrd 2332 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | neeqtri 2333 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | neeqtrd 2334 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | neeqtrri 2335 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | neeqtrrd 2336 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
|
|
Theorem | eqnetrrid 2337 |
B chained equality inference for inequality. (Contributed by NM,
6-Jun-2012.)
|
|
|
Theorem | 3netr3d 2338 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
|
|
Theorem | 3netr4d 2339 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
|
|
Theorem | 3netr3g 2340 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
|
|
Theorem | 3netr4g 2341 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14-Jun-2012.)
|
|
|
Theorem | necon3abii 2342 |
Deduction from equality to inequality. (Contributed by NM,
9-Nov-2007.)
|
|
|
Theorem | necon3bbii 2343 |
Deduction from equality to inequality. (Contributed by NM,
13-Apr-2007.)
|
|
|
Theorem | necon3bii 2344 |
Inference from equality to inequality. (Contributed by NM,
23-Feb-2005.)
|
|
|
Theorem | necon3abid 2345 |
Deduction from equality to inequality. (Contributed by NM,
21-Mar-2007.)
|
|
|
Theorem | necon3bbid 2346 |
Deduction from equality to inequality. (Contributed by NM,
2-Jun-2007.)
|
|
|
Theorem | necon3bid 2347 |
Deduction from equality to inequality. (Contributed by NM,
23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
|
|
Theorem | necon3ad 2348 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
|
|
Theorem | necon3bd 2349 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
|
|
Theorem | necon3d 2350 |
Contrapositive law deduction for inequality. (Contributed by NM,
10-Jun-2006.)
|
|
|
Theorem | nesym 2351 |
Characterization of inequality in terms of reversed equality (see
bicom 139). (Contributed by BJ, 7-Jul-2018.)
|
|
|
Theorem | nesymi 2352 |
Inference associated with nesym 2351. (Contributed by BJ, 7-Jul-2018.)
|
|
|
Theorem | nesymir 2353 |
Inference associated with nesym 2351. (Contributed by BJ, 7-Jul-2018.)
|
|
|
Theorem | necon3i 2354 |
Contrapositive inference for inequality. (Contributed by NM,
9-Aug-2006.)
|
|
|
Theorem | necon3ai 2355 |
Contrapositive inference for inequality. (Contributed by NM,
23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
|
|
Theorem | necon3bi 2356 |
Contrapositive inference for inequality. (Contributed by NM,
1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
|
|
Theorem | necon1aidc 2357 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
DECID DECID |
|
Theorem | necon1bidc 2358 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
DECID DECID
|
|
Theorem | necon1idc 2359 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID
|
|
Theorem | necon2ai 2360 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
|
|
Theorem | necon2bi 2361 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
|
|
Theorem | necon2i 2362 |
Contrapositive inference for inequality. (Contributed by NM,
18-Mar-2007.)
|
|
|
Theorem | necon2ad 2363 |
Contrapositive inference for inequality. (Contributed by NM,
19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
|
|
Theorem | necon2bd 2364 |
Contrapositive inference for inequality. (Contributed by NM,
13-Apr-2007.)
|
|
|
Theorem | necon2d 2365 |
Contrapositive inference for inequality. (Contributed by NM,
28-Dec-2008.)
|
|
|
Theorem | necon1abiidc 2366 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID |
|
Theorem | necon1bbiidc 2367 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID
|
|
Theorem | necon1abiddc 2368 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID
DECID |
|
Theorem | necon1bbiddc 2369 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID
DECID
|
|
Theorem | necon2abiidc 2370 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID
|
|
Theorem | necon2bbiidc 2371 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID |
|
Theorem | necon2abiddc 2372 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID
DECID
|
|
Theorem | necon2bbiddc 2373 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID
DECID
|
|
Theorem | necon4aidc 2374 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID |
|
Theorem | necon4idc 2375 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID DECID
|
|
Theorem | necon4addc 2376 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
DECID
DECID |
|
Theorem | necon4bddc 2377 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
DECID DECID |
|
Theorem | necon4ddc 2378 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
DECID
DECID
|
|
Theorem | necon4abiddc 2379 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18-May-2018.)
|
DECID
DECID DECID
DECID |
|
Theorem | necon4bbiddc 2380 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
DECID DECID
DECID DECID
|
|
Theorem | necon4biddc 2381 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
DECID
DECID DECID
DECID |
|
Theorem | necon1addc 2382 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
DECID DECID |
|
Theorem | necon1bddc 2383 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
DECID
DECID
|
|
Theorem | necon1ddc 2384 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
DECID
DECID
|
|
Theorem | neneqad 2385 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2327. One-way deduction form of df-ne 2307.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | nebidc 2386 |
Contraposition law for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
DECID DECID |
|
Theorem | pm13.18 2387 |
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
|
|
Theorem | pm13.181 2388 |
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
|
|
Theorem | pm2.21ddne 2389 |
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28-Feb-2017.)
|
|
|
Theorem | necom 2390 |
Commutation of inequality. (Contributed by NM, 14-May-1999.)
|
|
|
Theorem | necomi 2391 |
Inference from commutative law for inequality. (Contributed by NM,
17-Oct-2012.)
|
|
|
Theorem | necomd 2392 |
Deduction from commutative law for inequality. (Contributed by NM,
12-Feb-2008.)
|
|
|
Theorem | neanior 2393 |
A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|
|
|
Theorem | ne3anior 2394 |
A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
(Proof rewritten by Jim Kingdon, 19-May-2018.)
|
|
|
Theorem | nemtbir 2395 |
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13-Apr-2007.)
|
|
|
Theorem | nelne1 2396 |
Two classes are different if they don't contain the same element.
(Contributed by NM, 3-Feb-2012.)
|
|
|
Theorem | nelne2 2397 |
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25-Jun-2012.)
|
|
|
Theorem | nelelne 2398 |
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.)
|
|
|
Theorem | nfne 2399 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
|
|
Theorem | nfned 2400 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
|