Theorem List for Intuitionistic Logic Explorer - 2301-2400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | neneqd 2301 |
Deduction eliminating inequality definition. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
|
Theorem | neneq 2302 |
From inequality to non-equality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
|
Theorem | eqnetri 2303 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | eqnetrd 2304 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | eqnetrri 2305 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 |
|
Theorem | eqnetrrd 2306 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
|
Theorem | neeqtri 2307 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrd 2308 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | neeqtrri 2309 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrrd 2310 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | syl5eqner 2311 |
B chained equality inference for inequality. (Contributed by NM,
6-Jun-2012.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | 3netr3d 2312 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4d 2313 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr3g 2314 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4g 2315 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14-Jun-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | necon3abii 2316 |
Deduction from equality to inequality. (Contributed by NM,
9-Nov-2007.)
|
⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
|
Theorem | necon3bbii 2317 |
Deduction from equality to inequality. (Contributed by NM,
13-Apr-2007.)
|
⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
|
Theorem | necon3bii 2318 |
Inference from equality to inequality. (Contributed by NM,
23-Feb-2005.)
|
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
|
Theorem | necon3abid 2319 |
Deduction from equality to inequality. (Contributed by NM,
21-Mar-2007.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
|
Theorem | necon3bbid 2320 |
Deduction from equality to inequality. (Contributed by NM,
2-Jun-2007.)
|
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | necon3bid 2321 |
Deduction from equality to inequality. (Contributed by NM,
23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
|
Theorem | necon3ad 2322 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
|
Theorem | necon3bd 2323 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon3d 2324 |
Contrapositive law deduction for inequality. (Contributed by NM,
10-Jun-2006.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)) |
|
Theorem | nesym 2325 |
Characterization of inequality in terms of reversed equality (see
bicom 139). (Contributed by BJ, 7-Jul-2018.)
|
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
|
Theorem | nesymi 2326 |
Inference associated with nesym 2325. (Contributed by BJ, 7-Jul-2018.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 |
|
Theorem | nesymir 2327 |
Inference associated with nesym 2325. (Contributed by BJ, 7-Jul-2018.)
|
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | necon3i 2328 |
Contrapositive inference for inequality. (Contributed by NM,
9-Aug-2006.)
|
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
|
Theorem | necon3ai 2329 |
Contrapositive inference for inequality. (Contributed by NM,
23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
|
Theorem | necon3bi 2330 |
Contrapositive inference for inequality. (Contributed by NM,
1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon1aidc 2331 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 → 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 → 𝜑)) |
|
Theorem | necon1bidc 2332 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 → 𝐴 = 𝐵)) |
|
Theorem | necon1idc 2333 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
|
Theorem | necon2ai 2334 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
⊢ (𝐴 = 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon2bi 2335 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
|
Theorem | necon2i 2336 |
Contrapositive inference for inequality. (Contributed by NM,
18-Mar-2007.)
|
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵) |
|
Theorem | necon2ad 2337 |
Contrapositive inference for inequality. (Contributed by NM,
19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon2bd 2338 |
Contrapositive inference for inequality. (Contributed by NM,
13-Apr-2007.)
|
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
|
Theorem | necon2d 2339 |
Contrapositive inference for inequality. (Contributed by NM,
28-Dec-2008.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon1abiidc 2340 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜑)) |
|
Theorem | necon1bbiidc 2341 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) |
|
Theorem | necon1abiddc 2342 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ 𝜓))) |
|
Theorem | necon1bbiddc 2343 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) |
|
Theorem | necon2abiidc 2344 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) ⇒ ⊢ (DECID 𝜑 → (𝜑 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | necon2bbiidc 2345 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝜑 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) |
|
Theorem | necon2abiddc 2346 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝜓 ↔ 𝐴 ≠ 𝐵))) |
|
Theorem | necon2bbiddc 2347 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 ↔ 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) |
|
Theorem | necon4aidc 2348 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝜑 → 𝐴 = 𝐵)) |
|
Theorem | necon4idc 2349 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
|
Theorem | necon4addc 2350 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 → 𝐴 = 𝐵))) |
|
Theorem | necon4bddc 2351 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 → 𝜓))) |
|
Theorem | necon4ddc 2352 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵))) |
|
Theorem | necon4abiddc 2353 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ 𝜓)))) |
|
Theorem | necon4bbiddc 2354 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (𝜓 ↔ 𝐴 = 𝐵)))) |
|
Theorem | necon4biddc 2355 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))) |
|
Theorem | necon1addc 2356 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 → 𝜓))) |
|
Theorem | necon1bddc 2357 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 → 𝐴 = 𝐵))) |
|
Theorem | necon1ddc 2358 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))) |
|
Theorem | neneqad 2359 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2301. One-way deduction form of df-ne 2281.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | nebidc 2360 |
Contraposition law for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) |
|
Theorem | pm13.18 2361 |
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | pm13.181 2362 |
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) |
|
Theorem | pm2.21ddne 2363 |
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | necom 2364 |
Commutation of inequality. (Contributed by NM, 14-May-1999.)
|
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
|
Theorem | necomi 2365 |
Inference from commutative law for inequality. (Contributed by NM,
17-Oct-2012.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | necomd 2366 |
Deduction from commutative law for inequality. (Contributed by NM,
12-Feb-2008.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
|
Theorem | neanior 2367 |
A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
|
Theorem | ne3anior 2368 |
A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
(Proof rewritten by Jim Kingdon, 19-May-2018.)
|
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) |
|
Theorem | nemtbir 2369 |
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13-Apr-2007.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | nelne1 2370 |
Two classes are different if they don't contain the same element.
(Contributed by NM, 3-Feb-2012.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | nelne2 2371 |
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25-Jun-2012.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | nelelne 2372 |
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 2373 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
|
Theorem | nfned 2374 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ≠ 𝐵) |
|
2.1.4.2 Negated membership
|
|
Syntax | wnel 2375 |
Extend wff notation to include negated membership.
|
wff 𝐴 ∉ 𝐵 |
|
Definition | df-nel 2376 |
Define negated membership. (Contributed by NM, 7-Aug-1994.)
|
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
|
Theorem | neli 2377 |
Inference associated with df-nel 2376. (Contributed by BJ,
7-Jul-2018.)
|
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 |
|
Theorem | nelir 2378 |
Inference associated with df-nel 2376. (Contributed by BJ,
7-Jul-2018.)
|
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 |
|
Theorem | neleq1 2379 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
|
Theorem | neleq2 2380 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) |
|
Theorem | neleq12d 2381 |
Equality theorem for negated membership. (Contributed by FL,
10-Aug-2016.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) |
|
Theorem | nfnel 2382 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 |
|
Theorem | nfneld 2383 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) |
|
Theorem | elnelne1 2384 |
Two classes are different if they don't contain the same element.
(Contributed by AV, 28-Jan-2020.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | elnelne2 2385 |
Two classes are different if they don't belong to the same class.
(Contributed by AV, 28-Jan-2020.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | nelcon3d 2386 |
Contrapositive law deduction for negated membership. (Contributed by
AV, 28-Jan-2020.)
|
⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) |
|
Theorem | elnelall 2387 |
A contradiction concerning membership implies anything. (Contributed by
Alexander van der Vekens, 25-Jan-2018.)
|
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) |
|
2.1.5 Restricted quantification
|
|
Syntax | wral 2388 |
Extend wff notation to include restricted universal quantification.
|
wff ∀𝑥 ∈ 𝐴 𝜑 |
|
Syntax | wrex 2389 |
Extend wff notation to include restricted existential quantification.
|
wff ∃𝑥 ∈ 𝐴 𝜑 |
|
Syntax | wreu 2390 |
Extend wff notation to include restricted existential uniqueness.
|
wff ∃!𝑥 ∈ 𝐴 𝜑 |
|
Syntax | wrmo 2391 |
Extend wff notation to include restricted "at most one."
|
wff ∃*𝑥 ∈ 𝐴 𝜑 |
|
Syntax | crab 2392 |
Extend class notation to include the restricted class abstraction (class
builder).
|
class {𝑥 ∈ 𝐴 ∣ 𝜑} |
|
Definition | df-ral 2393 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19-Aug-1993.)
|
⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
|
Definition | df-rex 2394 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30-Aug-1993.)
|
⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
|
Definition | df-reu 2395 |
Define restricted existential uniqueness. (Contributed by NM,
22-Nov-1994.)
|
⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
|
Definition | df-rmo 2396 |
Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|
⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
|
Definition | df-rab 2397 |
Define a restricted class abstraction (class builder), which is the class
of all 𝑥 in 𝐴 such that 𝜑 is true. Definition of
[TakeutiZaring] p. 20. (Contributed
by NM, 22-Nov-1994.)
|
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} |
|
Theorem | ralnex 2398 |
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21-Jan-1997.)
|
⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
|
Theorem | rexnalim 2399 |
Relationship between restricted universal and existential quantifiers. In
classical logic this would be a biconditional. (Contributed by Jim
Kingdon, 17-Aug-2018.)
|
⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀𝑥 ∈ 𝐴 𝜑) |
|
Theorem | dfrex2dc 2400 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 29-Jun-2022.)
|
⊢ (DECID ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)) |