Theorem List for Intuitionistic Logic Explorer - 2201-2300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cleqf 2201 |
Establish equality between classes, using bound-variable hypotheses
instead of distinct variable conditions. See also cleqh 2137.
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
|
Theorem | abid2f 2202 |
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 2203* |
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
|
|
Syntax | wne 2204 |
Extend wff notation to include inequality.
|
wff 𝐴 ≠ 𝐵 |
|
Syntax | wnel 2205 |
Extend wff notation to include negated membership.
|
wff 𝐴 ∉ 𝐵 |
|
Definition | df-ne 2206 |
Define inequality. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
|
Definition | df-nel 2207 |
Define negated membership. (Contributed by NM, 7-Aug-1994.)
|
⊢ (𝐴 ∉ 𝐵 ↔ ¬ 𝐴 ∈ 𝐵) |
|
2.1.4.1 Negated equality
|
|
Theorem | neii 2208 |
Inference associated with df-ne 2206. (Contributed by BJ, 7-Jul-2018.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐴 = 𝐵 |
|
Theorem | neir 2209 |
Inference associated with df-ne 2206. (Contributed by BJ, 7-Jul-2018.)
|
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 |
|
Theorem | nner 2210 |
Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵) |
|
Theorem | nnedc 2211 |
Negation of inequality where equality is decidable. (Contributed by Jim
Kingdon, 15-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | dcned 2212 |
Decidable equality implies decidable negated equality. (Contributed by
Jim Kingdon, 3-May-2020.)
|
⊢ (𝜑 → DECID 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵) |
|
Theorem | neqned 2213 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2226. One-way deduction form of df-ne 2206.
(Contributed by David Moews, 28-Feb-2017.) Allow a shortening of
necon3bi 2255. (Revised by Wolf Lammen, 22-Nov-2019.)
|
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | neqne 2214 |
From non equality to inequality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵) |
|
Theorem | neirr 2215 |
No class is unequal to itself. (Contributed by Stefan O'Rear,
1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ ¬ 𝐴 ≠ 𝐴 |
|
Theorem | dcne 2216 |
Decidable equality expressed in terms of ≠.
Basically the same as
df-dc 743. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)) |
|
Theorem | nonconne 2217 |
Law of noncontradiction with equality and inequality. (Contributed by NM,
3-Feb-2012.)
|
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵) |
|
Theorem | neeq1 2218 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
|
Theorem | neeq2 2219 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
|
Theorem | neeq1i 2220 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
|
Theorem | neeq2i 2221 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵) |
|
Theorem | neeq12i 2222 |
Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
|
Theorem | neeq1d 2223 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
|
Theorem | neeq2d 2224 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
|
Theorem | neeq12d 2225 |
Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) |
|
Theorem | neneqd 2226 |
Deduction eliminating inequality definition. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
|
Theorem | neneq 2227 |
From inequality to non equality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
|
Theorem | eqnetri 2228 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | eqnetrd 2229 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | eqnetrri 2230 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 |
|
Theorem | eqnetrrd 2231 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
|
Theorem | neeqtri 2232 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrd 2233 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | neeqtrri 2234 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrrd 2235 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | syl5eqner 2236 |
B chained equality inference for inequality. (Contributed by NM,
6-Jun-2012.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | 3netr3d 2237 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4d 2238 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr3g 2239 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4g 2240 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14-Jun-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | necon3abii 2241 |
Deduction from equality to inequality. (Contributed by NM,
9-Nov-2007.)
|
⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
|
Theorem | necon3bbii 2242 |
Deduction from equality to inequality. (Contributed by NM,
13-Apr-2007.)
|
⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
|
Theorem | necon3bii 2243 |
Inference from equality to inequality. (Contributed by NM,
23-Feb-2005.)
|
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
|
Theorem | necon3abid 2244 |
Deduction from equality to inequality. (Contributed by NM,
21-Mar-2007.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
|
Theorem | necon3bbid 2245 |
Deduction from equality to inequality. (Contributed by NM,
2-Jun-2007.)
|
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | necon3bid 2246 |
Deduction from equality to inequality. (Contributed by NM,
23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
|
Theorem | necon3ad 2247 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
|
Theorem | necon3bd 2248 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon3d 2249 |
Contrapositive law deduction for inequality. (Contributed by NM,
10-Jun-2006.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)) |
|
Theorem | nesym 2250 |
Characterization of inequality in terms of reversed equality (see
bicom 128). (Contributed by BJ, 7-Jul-2018.)
|
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
|
Theorem | nesymi 2251 |
Inference associated with nesym 2250. (Contributed by BJ, 7-Jul-2018.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 |
|
Theorem | nesymir 2252 |
Inference associated with nesym 2250. (Contributed by BJ, 7-Jul-2018.)
|
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | necon3i 2253 |
Contrapositive inference for inequality. (Contributed by NM,
9-Aug-2006.)
|
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
|
Theorem | necon3ai 2254 |
Contrapositive inference for inequality. (Contributed by NM,
23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
|
Theorem | necon3bi 2255 |
Contrapositive inference for inequality. (Contributed by NM,
1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon1aidc 2256 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 → 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 → 𝜑)) |
|
Theorem | necon1bidc 2257 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 → 𝐴 = 𝐵)) |
|
Theorem | necon1idc 2258 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
|
Theorem | necon2ai 2259 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
⊢ (𝐴 = 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon2bi 2260 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |
|
Theorem | necon2i 2261 |
Contrapositive inference for inequality. (Contributed by NM,
18-Mar-2007.)
|
⊢ (𝐴 = 𝐵 → 𝐶 ≠ 𝐷) ⇒ ⊢ (𝐶 = 𝐷 → 𝐴 ≠ 𝐵) |
|
Theorem | necon2ad 2262 |
Contrapositive inference for inequality. (Contributed by NM,
19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon2bd 2263 |
Contrapositive inference for inequality. (Contributed by NM,
13-Apr-2007.)
|
⊢ (𝜑 → (𝜓 → 𝐴 ≠ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ 𝜓)) |
|
Theorem | necon2d 2264 |
Contrapositive inference for inequality. (Contributed by NM,
28-Dec-2008.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 = 𝐷 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon1abiidc 2265 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 ↔ 𝜑)) |
|
Theorem | necon1bbiidc 2266 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 ↔ 𝐴 = 𝐵)) |
|
Theorem | necon1abiddc 2267 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ 𝜓))) |
|
Theorem | necon1bbiddc 2268 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 ↔ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 = 𝐵))) |
|
Theorem | necon2abiidc 2269 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) ⇒ ⊢ (DECID 𝜑 → (𝜑 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | necon2bbii 2270 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝜑 ↔ 𝐴 ≠ 𝐵)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜑)) |
|
Theorem | necon2abiddc 2271 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝜓 ↔ 𝐴 ≠ 𝐵))) |
|
Theorem | necon2bbiddc 2272 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 ↔ 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 = 𝐵 ↔ ¬ 𝜓))) |
|
Theorem | necon4aidc 2273 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝜑 → 𝐴 = 𝐵)) |
|
Theorem | necon4idc 2274 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵)) |
|
Theorem | necon4addc 2275 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ¬ 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝜓 → 𝐴 = 𝐵))) |
|
Theorem | necon4bddc 2276 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 ≠ 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 = 𝐵 → 𝜓))) |
|
Theorem | necon4ddc 2277 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 ≠ 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 = 𝐷 → 𝐴 = 𝐵))) |
|
Theorem | necon4abiddc 2278 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝜓 → (𝐴 = 𝐵 ↔ 𝜓)))) |
|
Theorem | necon4bbiddc 2279 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (DECID
𝐴 = 𝐵 → (𝜓 ↔ 𝐴 = 𝐵)))) |
|
Theorem | necon4biddc 2280 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)))) |
|
Theorem | necon1addc 2281 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (𝜑 → (DECID 𝜓 → (¬ 𝜓 → 𝐴 = 𝐵))) ⇒ ⊢ (𝜑 → (DECID 𝜓 → (𝐴 ≠ 𝐵 → 𝜓))) |
|
Theorem | necon1bddc 2282 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜓))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (¬ 𝜓 → 𝐴 = 𝐵))) |
|
Theorem | necon1ddc 2283 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝐶 = 𝐷))) ⇒ ⊢ (𝜑 → (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵))) |
|
Theorem | neneqad 2284 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2226. One-way deduction form of df-ne 2206.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | nebidc 2285 |
Contraposition law for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (DECID 𝐶 = 𝐷 → ((𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ↔ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)))) |
|
Theorem | pm13.18 2286 |
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | pm13.181 2287 |
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
⊢ ((𝐴 = 𝐵 ∧ 𝐵 ≠ 𝐶) → 𝐴 ≠ 𝐶) |
|
Theorem | pm2.21ddne 2288 |
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28-Feb-2017.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | necom 2289 |
Commutation of inequality. (Contributed by NM, 14-May-1999.)
|
⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴) |
|
Theorem | necomi 2290 |
Inference from commutative law for inequality. (Contributed by NM,
17-Oct-2012.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | necomd 2291 |
Deduction from commutative law for inequality. (Contributed by NM,
12-Feb-2008.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐴) |
|
Theorem | neanior 2292 |
A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
|
Theorem | ne3anior 2293 |
A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
(Proof rewritten by Jim Kingdon, 19-May-2018.)
|
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷 ∧ 𝐸 ≠ 𝐹) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷 ∨ 𝐸 = 𝐹)) |
|
Theorem | nemtbir 2294 |
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13-Apr-2007.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | nelne1 2295 |
Two classes are different if they don't contain the same element.
(Contributed by NM, 3-Feb-2012.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶) → 𝐵 ≠ 𝐶) |
|
Theorem | nelne2 2296 |
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25-Jun-2012.)
|
⊢ ((𝐴 ∈ 𝐶 ∧ ¬ 𝐵 ∈ 𝐶) → 𝐴 ≠ 𝐵) |
|
Theorem | nfne 2297 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
|
Theorem | nfned 2298 |
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
|
|
Theorem | neli 2299 |
Inference associated with df-nel 2207. (Contributed by BJ,
7-Jul-2018.)
|
⊢ 𝐴 ∉ 𝐵 ⇒ ⊢ ¬ 𝐴 ∈ 𝐵 |
|
Theorem | nelir 2300 |
Inference associated with df-nel 2207. (Contributed by BJ,
7-Jul-2018.)
|
⊢ ¬ 𝐴 ∈ 𝐵 ⇒ ⊢ 𝐴 ∉ 𝐵 |