Theorem List for Intuitionistic Logic Explorer - 2401-2500 *Has distinct variable
group(s)
| Type | Label | Description |
| Statement |
| |
| Theorem | 3netr3g 2401 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
| ⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
| |
| Theorem | 3netr4g 2402 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14-Jun-2012.)
|
| ⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
| |
| Theorem | necon3abii 2403 |
Deduction from equality to inequality. (Contributed by NM,
9-Nov-2007.)
|
| ⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
| |
| Theorem | necon3bbii 2404 |
Deduction from equality to inequality. (Contributed by NM,
13-Apr-2007.)
|
| ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
| |
| Theorem | necon3bii 2405 |
Inference from equality to inequality. (Contributed by NM,
23-Feb-2005.)
|
| ⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
| |
| Theorem | necon3abid 2406 |
Deduction from equality to inequality. (Contributed by NM,
21-Mar-2007.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
| |
| Theorem | necon3bbid 2407 |
Deduction from equality to inequality. (Contributed by NM,
2-Jun-2007.)
|
| ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
| |
| Theorem | necon3bid 2408 |
Deduction from equality to inequality. (Contributed by NM,
23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
| |
| Theorem | necon3ad 2409 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
| ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
| |
| Theorem | necon3bd 2410 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
| |
| Theorem | necon3d 2411 |
Contrapositive law deduction for inequality. (Contributed by NM,
10-Jun-2006.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)) |
| |
| Theorem | nesym 2412 |
Characterization of inequality in terms of reversed equality (see
bicom 140). (Contributed by BJ, 7-Jul-2018.)
|
| ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
| |
| Theorem | nesymi 2413 |
Inference associated with nesym 2412. (Contributed by BJ, 7-Jul-2018.)
|
| ⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 |
| |
| Theorem | nesymir 2414 |
Inference associated with nesym 2412. (Contributed by BJ, 7-Jul-2018.)
|
| ⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
| |
| Theorem | necon3i 2415 |
Contrapositive inference for inequality. (Contributed by NM,
9-Aug-2006.)
|
| ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
| |
| Theorem | necon3ai 2416 |
Contrapositive inference for inequality. (Contributed by NM,
23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
| |
| Theorem | necon3bi 2417 |
Contrapositive inference for inequality. (Contributed by NM,
1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
| ⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
| |
| Theorem | necon1aidc 2418 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
| ⊢ (DECID 𝜑 → (¬ 𝜑 → 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 → 𝜑)) |
| |
| Theorem | necon1bidc 2419 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 → 𝐴 = 𝐵)) |
| |
| Theorem | necon1idc 2420 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
| |
| Theorem | necon2ai 2421 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
| ⊢ (𝐴 = 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
| |
| Theorem | necon2bi 2422 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
| ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
| |
| Theorem | necon2i 2423 |
Contrapositive inference for inequality. (Contributed by NM,
18-Mar-2007.)
|
| ⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵) |
| |
| Theorem | necon2ad 2424 |
Contrapositive inference for inequality. (Contributed by NM,
19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
| |
| Theorem | necon2bd 2425 |
Contrapositive inference for inequality. (Contributed by NM,
13-Apr-2007.)
|
| ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
| |
| Theorem | necon2d 2426 |
Contrapositive inference for inequality. (Contributed by NM,
28-Dec-2008.)
|
| ⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
| |
| Theorem | necon1abiidc 2427 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝜑 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜑)) |
| |
| Theorem | necon1bbiidc 2428 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) |
| |
| Theorem | necon1abiddc 2429 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ 𝜓))) |
| |
| Theorem | necon1bbiddc 2430 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) |
| |
| Theorem | necon2abiidc 2431 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) ⇒ ⊢ (DECID 𝜑 → (𝜑 ↔ 𝐴 ≠ 𝐵)) |
| |
| Theorem | necon2bbiidc 2432 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (𝜑 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) |
| |
| Theorem | necon2abiddc 2433 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝜓 ↔ 𝐴 ≠ 𝐵))) |
| |
| Theorem | necon2bbiddc 2434 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 ↔ 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) |
| |
| Theorem | necon4aidc 2435 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝜑 → 𝐴 = 𝐵)) |
| |
| Theorem | necon4idc 2436 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
| |
| Theorem | necon4addc 2437 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 → 𝐴 = 𝐵))) |
| |
| Theorem | necon4bddc 2438 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 → 𝜓))) |
| |
| Theorem | necon4ddc 2439 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵))) |
| |
| Theorem | necon4abiddc 2440 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ 𝜓)))) |
| |
| Theorem | necon4bbiddc 2441 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (𝜓 ↔ 𝐴 = 𝐵)))) |
| |
| Theorem | necon4biddc 2442 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))) |
| |
| Theorem | necon1addc 2443 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 → 𝜓))) |
| |
| Theorem | necon1bddc 2444 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 → 𝐴 = 𝐵))) |
| |
| Theorem | necon1ddc 2445 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
| ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))) |
| |
| Theorem | neneqad 2446 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2388. One-way deduction form of df-ne 2368.
(Contributed by David Moews, 28-Feb-2017.)
|
| ⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
| |
| Theorem | nebidc 2447 |
Contraposition law for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
| ⊢ (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) |
| |
| Theorem | pm13.18 2448 |
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
| ⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
| |
| Theorem | pm13.181 2449 |
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
| ⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) |
| |
| Theorem | pm2.21ddne 2450 |
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28-Feb-2017.)
|
| ⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) |
| |
| Theorem | necom 2451 |
Commutation of inequality. (Contributed by NM, 14-May-1999.)
|
| ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
| |
| Theorem | necomi 2452 |
Inference from commutative law for inequality. (Contributed by NM,
17-Oct-2012.)
|
| ⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
| |
| Theorem | necomd 2453 |
Deduction from commutative law for inequality. (Contributed by NM,
12-Feb-2008.)
|
| ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
| |
| Theorem | neanior 2454 |
A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|
| ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
| |
| Theorem | ne3anior 2455 |
A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
(Proof rewritten by Jim Kingdon, 19-May-2018.)
|
| ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) |
| |
| Theorem | nemtbir 2456 |
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13-Apr-2007.)
|
| ⊢ 𝐴 ≠ 𝐵
& ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 |
| |
| Theorem | nelne1 2457 |
Two classes are different if they don't contain the same element.
(Contributed by NM, 3-Feb-2012.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
| |
| Theorem | nelne2 2458 |
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25-Jun-2012.)
|
| ⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
| |
| Theorem | nelelne 2459 |
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 2460 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
| ⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
| |
| Theorem | nfned 2461 |
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 2462 |
Extend wff notation to include negated membership.
|
| wff 𝐴 ∉ 𝐵 |
| |
| Definition | df-nel 2463 |
Define negated membership. (Contributed by NM, 7-Aug-1994.)
|
| ⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
| |
| Theorem | neli 2464 |
Inference associated with df-nel 2463. (Contributed by BJ,
7-Jul-2018.)
|
| ⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 |
| |
| Theorem | nelir 2465 |
Inference associated with df-nel 2463. (Contributed by BJ,
7-Jul-2018.)
|
| ⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 |
| |
| Theorem | neleq1 2466 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
| ⊢ (𝐴 = 𝐵 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐶)) |
| |
| Theorem | neleq2 2467 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
| ⊢ (𝐴 = 𝐵 → (𝐶 ∉ 𝐴 ↔ 𝐶 ∉ 𝐵)) |
| |
| Theorem | neleq12d 2468 |
Equality theorem for negated membership. (Contributed by FL,
10-Aug-2016.)
|
| ⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ∉ 𝐶 ↔ 𝐵 ∉ 𝐷)) |
| |
| Theorem | nfnel 2469 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
| ⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∉ 𝐵 |
| |
| Theorem | nfneld 2470 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
| ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∉ 𝐵) |
| |
| Theorem | elnelne1 2471 |
Two classes are different if they don't contain the same element.
(Contributed by AV, 28-Jan-2020.)
|
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∉ 𝐶) → 𝐵 ≠ 𝐶) |
| |
| Theorem | elnelne2 2472 |
Two classes are different if they don't belong to the same class.
(Contributed by AV, 28-Jan-2020.)
|
| ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∉ 𝐶) → 𝐴 ≠ 𝐵) |
| |
| Theorem | nelcon3d 2473 |
Contrapositive law deduction for negated membership. (Contributed by
AV, 28-Jan-2020.)
|
| ⊢ (𝜑 → (𝐴 ∈ 𝐵 → 𝐶 ∈ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ∉ 𝐷 → 𝐴 ∉ 𝐵)) |
| |
| Theorem | elnelall 2474 |
A contradiction concerning membership implies anything. (Contributed by
Alexander van der Vekens, 25-Jan-2018.)
|
| ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∉ 𝐵 → 𝜑)) |
| |
| 2.1.5 Restricted quantification
|
| |
| Syntax | wral 2475 |
Extend wff notation to include restricted universal quantification.
|
| wff ∀𝑥 ∈ 𝐴 𝜑 |
| |
| Syntax | wrex 2476 |
Extend wff notation to include restricted existential quantification.
|
| wff ∃𝑥 ∈ 𝐴 𝜑 |
| |
| Syntax | wreu 2477 |
Extend wff notation to include restricted existential uniqueness.
|
| wff ∃!𝑥 ∈ 𝐴 𝜑 |
| |
| Syntax | wrmo 2478 |
Extend wff notation to include restricted "at most one".
|
| wff ∃*𝑥 ∈ 𝐴 𝜑 |
| |
| Syntax | crab 2479 |
Extend class notation to include the restricted class abstraction (class
builder).
|
| class {𝑥 ∈ 𝐴 ∣ 𝜑} |
| |
| Definition | df-ral 2480 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19-Aug-1993.)
|
| ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) |
| |
| Definition | df-rex 2481 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30-Aug-1993.)
|
| ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| |
| Definition | df-reu 2482 |
Define restricted existential uniqueness. (Contributed by NM,
22-Nov-1994.)
|
| ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| |
| Definition | df-rmo 2483 |
Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|
| ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
| |
| Definition | df-rab 2484 |
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 2485 |
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21-Jan-1997.)
|
| ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑) |
| |
| Theorem | rexnalim 2486 |
Relationship between restricted universal and existential quantifiers. In
classical logic this would be a biconditional. (Contributed by Jim
Kingdon, 17-Aug-2018.)
|
| ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀𝑥 ∈ 𝐴 𝜑) |
| |
| Theorem | nnral 2487 |
The double negation of a universal quantification implies the universal
quantification of the double negation. Restricted quantifier version of
nnal 1663. (Contributed by Jim Kingdon, 1-Aug-2024.)
|
| ⊢ (¬ ¬ ∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 ¬ ¬ 𝜑) |
| |
| Theorem | dfrex2dc 2488 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 29-Jun-2022.)
|
| ⊢ (DECID ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)) |
| |
| Theorem | ralexim 2489 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
| ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ¬ ∃𝑥 ∈ 𝐴 ¬ 𝜑) |
| |
| Theorem | rexalim 2490 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
| ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
| |
| Theorem | ralbida 2491 |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 6-Oct-2003.)
|
| ⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | rexbida 2492 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 6-Oct-2003.)
|
| ⊢ Ⅎ𝑥𝜑
& ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | ralbidva 2493* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 4-Mar-1997.)
|
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | rexbidva 2494* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 9-Mar-1997.)
|
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | ralbid 2495 |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 27-Jun-1998.)
|
| ⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | rexbid 2496 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 27-Jun-1998.)
|
| ⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | ralbidv 2497* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 20-Nov-1994.)
|
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | rexbidv 2498* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 20-Nov-1994.)
|
| ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
| |
| Theorem | ralbidv2 2499* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 6-Apr-1997.)
|
| ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
| |
| Theorem | rexbidv2 2500* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 22-May-1999.)
|
| ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |