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