Theorem List for Intuitionistic Logic Explorer - 2201-2300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | cbvab 2201 |
Rule used to change bound variables, using implicit substitution.
(Contributed by Andrew Salmon, 11-Jul-2011.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
|
Theorem | cbvabv 2202* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 26-May-1999.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓} |
|
Theorem | clelab 2203* |
Membership of a class variable in a class abstraction. (Contributed by
NM, 23-Dec-1993.)
|
⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
|
Theorem | clabel 2204* |
Membership of a class abstraction in another class. (Contributed by NM,
17-Jan-2006.)
|
⊢ ({𝑥 ∣ 𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝑦 ↔ 𝜑))) |
|
Theorem | sbab 2205* |
The right-hand side of the second equality is a way of representing
proper substitution of 𝑦 for 𝑥 into a class variable.
(Contributed by NM, 14-Sep-2003.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = {𝑧 ∣ [𝑦 / 𝑥]𝑧 ∈ 𝐴}) |
|
2.1.3 Class form not-free predicate
|
|
Syntax | wnfc 2206 |
Extend wff definition to include the not-free predicate for classes.
|
wff Ⅎ𝑥𝐴 |
|
Theorem | nfcjust 2207* |
Justification theorem for df-nfc 2208. (Contributed by Mario Carneiro,
13-Oct-2016.)
|
⊢ (∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴 ↔ ∀𝑧Ⅎ𝑥 𝑧 ∈ 𝐴) |
|
Definition | df-nfc 2208* |
Define the not-free predicate for classes. This is read "𝑥 is not
free in 𝐴". Not-free means that the
value of 𝑥 cannot affect
the value of 𝐴, e.g., any occurrence of 𝑥 in
𝐴
is
effectively bound by a quantifier or something that expands to one (such
as "there exists at most one"). It is defined in terms of the
not-free
predicate df-nf 1390 for wffs; see that definition for more
information.
(Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) |
|
Theorem | nfci 2209* |
Deduce that a class 𝐴 does not have 𝑥 free in it.
(Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 ⇒ ⊢ Ⅎ𝑥𝐴 |
|
Theorem | nfcii 2210* |
Deduce that a class 𝐴 does not have 𝑥 free in it.
(Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ Ⅎ𝑥𝐴 |
|
Theorem | nfcr 2211* |
Consequence of the not-free predicate. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ (Ⅎ𝑥𝐴 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
|
Theorem | nfcrii 2212* |
Consequence of the not-free predicate. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
|
Theorem | nfcri 2213* |
Consequence of the not-free predicate. (Note that unlike nfcr 2211,
this
does not require 𝑦 and 𝐴 to be disjoint.)
(Contributed by Mario
Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
|
Theorem | nfcd 2214* |
Deduce that a class 𝐴 does not have 𝑥 free in it.
(Contributed
by Mario Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) |
|
Theorem | nfceqi 2215 |
Equality theorem for class not-free. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵) |
|
Theorem | nfcxfr 2216 |
A utility lemma to transfer a bound-variable hypothesis builder into a
definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ 𝐴 = 𝐵
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥𝐴 |
|
Theorem | nfcxfrd 2217 |
A utility lemma to transfer a bound-variable hypothesis builder into a
definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ 𝐴 = 𝐵
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝐴) |
|
Theorem | nfceqdf 2218 |
An equality theorem for effectively not free. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)) |
|
Theorem | nfcv 2219* |
If 𝑥 is disjoint from 𝐴, then
𝑥
is not free in 𝐴.
(Contributed by Mario Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴 |
|
Theorem | nfcvd 2220* |
If 𝑥 is disjoint from 𝐴, then
𝑥
is not free in 𝐴.
(Contributed by Mario Carneiro, 7-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) |
|
Theorem | nfab1 2221 |
Bound-variable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} |
|
Theorem | nfnfc1 2222 |
𝑥
is bound in Ⅎ𝑥𝐴. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ Ⅎ𝑥Ⅎ𝑥𝐴 |
|
Theorem | nfab 2223 |
Bound-variable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 11-Aug-2016.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥{𝑦 ∣ 𝜑} |
|
Theorem | nfaba1 2224 |
Bound-variable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 14-Oct-2016.)
|
⊢ Ⅎ𝑥{𝑦 ∣ ∀𝑥𝜑} |
|
Theorem | nfnfc 2225 |
Hypothesis builder for Ⅎ𝑦𝐴. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥Ⅎ𝑦𝐴 |
|
Theorem | nfeq 2226 |
Hypothesis builder for equality. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
|
Theorem | nfel 2227 |
Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
|
Theorem | nfeq1 2228* |
Hypothesis builder for equality, special case. (Contributed by Mario
Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
|
Theorem | nfel1 2229* |
Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
|
Theorem | nfeq2 2230* |
Hypothesis builder for equality, special case. (Contributed by Mario
Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
|
Theorem | nfel2 2231* |
Hypothesis builder for elementhood, special case. (Contributed by Mario
Carneiro, 10-Oct-2016.)
|
⊢ Ⅎ𝑥𝐵 ⇒ ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵 |
|
Theorem | nfcrd 2232* |
Consequence of the not-free predicate. (Contributed by Mario Carneiro,
11-Aug-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝑦 ∈ 𝐴) |
|
Theorem | nfeqd 2233 |
Hypothesis builder for equality. (Contributed by Mario Carneiro,
7-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 = 𝐵) |
|
Theorem | nfeld 2234 |
Hypothesis builder for elementhood. (Contributed by Mario Carneiro,
7-Oct-2016.)
|
⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑥𝐵) ⇒ ⊢ (𝜑 → Ⅎ𝑥 𝐴 ∈ 𝐵) |
|
Theorem | drnfc1 2235 |
Formula-building lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8-Oct-2016.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝐴 ↔ Ⅎ𝑦𝐵)) |
|
Theorem | drnfc2 2236 |
Formula-building lemma for use with the Distinctor Reduction Theorem.
(Contributed by Mario Carneiro, 8-Oct-2016.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝐴 ↔ Ⅎ𝑧𝐵)) |
|
Theorem | nfabd 2237 |
Bound-variable hypothesis builder for a class abstraction. (Contributed
by Mario Carneiro, 8-Oct-2016.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥{𝑦 ∣ 𝜓}) |
|
Theorem | dvelimdc 2238 |
Deduction form of dvelimc 2239. (Contributed by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑧𝜑
& ⊢ (𝜑 → Ⅎ𝑥𝐴)
& ⊢ (𝜑 → Ⅎ𝑧𝐵)
& ⊢ (𝜑 → (𝑧 = 𝑦 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵)) |
|
Theorem | dvelimc 2239 |
Version of dvelim 1934 for classes. (Contributed by Mario Carneiro,
8-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑧𝐵
& ⊢ (𝑧 = 𝑦 → 𝐴 = 𝐵) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝐵) |
|
Theorem | nfcvf 2240 |
If 𝑥 and 𝑦 are distinct, then 𝑥 is not
free in 𝑦.
(Contributed by Mario Carneiro, 8-Oct-2016.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝑦) |
|
Theorem | nfcvf2 2241 |
If 𝑥 and 𝑦 are distinct, then 𝑦 is not
free in 𝑥.
(Contributed by Mario Carneiro, 5-Dec-2016.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
|
Theorem | cleqf 2242 |
Establish equality between classes, using bound-variable hypotheses
instead of distinct variable conditions. See also cleqh 2178.
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
⊢ Ⅎ𝑥𝐴
& ⊢ Ⅎ𝑥𝐵 ⇒ ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
|
Theorem | abid2f 2243 |
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 2244* |
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 2245 |
Extend wff notation to include inequality.
|
wff 𝐴 ≠ 𝐵 |
|
Definition | df-ne 2246 |
Define inequality. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) |
|
Theorem | neii 2247 |
Inference associated with df-ne 2246. (Contributed by BJ, 7-Jul-2018.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐴 = 𝐵 |
|
Theorem | neir 2248 |
Inference associated with df-ne 2246. (Contributed by BJ, 7-Jul-2018.)
|
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐵 |
|
Theorem | nner 2249 |
Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
|
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵) |
|
Theorem | nnedc 2250 |
Negation of inequality where equality is decidable. (Contributed by Jim
Kingdon, 15-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵)) |
|
Theorem | dcned 2251 |
Decidable equality implies decidable negated equality. (Contributed by
Jim Kingdon, 3-May-2020.)
|
⊢ (𝜑 → DECID 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → DECID 𝐴 ≠ 𝐵) |
|
Theorem | neqned 2252 |
If it is not the case that two classes are equal, they are unequal.
Converse of neneqd 2266. One-way deduction form of df-ne 2246.
(Contributed by David Moews, 28-Feb-2017.) Allow a shortening of
necon3bi 2295. (Revised by Wolf Lammen, 22-Nov-2019.)
|
⊢ (𝜑 → ¬ 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | neqne 2253 |
From non equality to inequality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵) |
|
Theorem | neirr 2254 |
No class is unequal to itself. (Contributed by Stefan O'Rear,
1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ ¬ 𝐴 ≠ 𝐴 |
|
Theorem | eqneqall 2255 |
A contradiction concerning equality implies anything. (Contributed by
Alexander van der Vekens, 25-Jan-2018.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) |
|
Theorem | dcne 2256 |
Decidable equality expressed in terms of ≠.
Basically the same as
df-dc 776. (Contributed by Jim Kingdon, 14-Mar-2020.)
|
⊢ (DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∨ 𝐴 ≠ 𝐵)) |
|
Theorem | nonconne 2257 |
Law of noncontradiction with equality and inequality. (Contributed by NM,
3-Feb-2012.)
|
⊢ ¬ (𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵) |
|
Theorem | neeq1 2258 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
|
Theorem | neeq2 2259 |
Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
|
⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
|
Theorem | neeq1i 2260 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
|
Theorem | neeq2i 2261 |
Inference for inequality. (Contributed by NM, 29-Apr-2005.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵) |
|
Theorem | neeq12i 2262 |
Inference for inequality. (Contributed by NM, 24-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐶 = 𝐷 ⇒ ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷) |
|
Theorem | neeq1d 2263 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
|
Theorem | neeq2d 2264 |
Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
|
Theorem | neeq12d 2265 |
Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐷)) |
|
Theorem | neneqd 2266 |
Deduction eliminating inequality definition. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
|
Theorem | neneq 2267 |
From inequality to non equality. (Contributed by Glauco Siliprandi,
11-Dec-2019.)
|
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
|
Theorem | eqnetri 2268 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐵 ≠ 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | eqnetrd 2269 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | eqnetrri 2270 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 = 𝐵
& ⊢ 𝐴 ≠ 𝐶 ⇒ ⊢ 𝐵 ≠ 𝐶 |
|
Theorem | eqnetrrd 2271 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 = 𝐵)
& ⊢ (𝜑 → 𝐴 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐵 ≠ 𝐶) |
|
Theorem | neeqtri 2272 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐵 = 𝐶 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrd 2273 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | neeqtrri 2274 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ 𝐴 ≠ 𝐵
& ⊢ 𝐶 = 𝐵 ⇒ ⊢ 𝐴 ≠ 𝐶 |
|
Theorem | neeqtrrd 2275 |
Substitution of equal classes into an inequality. (Contributed by NM,
4-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐵) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | syl5eqner 2276 |
B chained equality inference for inequality. (Contributed by NM,
6-Jun-2012.)
|
⊢ 𝐵 = 𝐴
& ⊢ (𝜑 → 𝐵 ≠ 𝐶) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐶) |
|
Theorem | 3netr3d 2277 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐴 = 𝐶)
& ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4d 2278 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ (𝜑 → 𝐶 = 𝐴)
& ⊢ (𝜑 → 𝐷 = 𝐵) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr3g 2279 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 24-Jul-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐴 = 𝐶
& ⊢ 𝐵 = 𝐷 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | 3netr4g 2280 |
Substitution of equality into both sides of an inequality. (Contributed
by NM, 14-Jun-2012.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵)
& ⊢ 𝐶 = 𝐴
& ⊢ 𝐷 = 𝐵 ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) |
|
Theorem | necon3abii 2281 |
Deduction from equality to inequality. (Contributed by NM,
9-Nov-2007.)
|
⊢ (𝐴 = 𝐵 ↔ 𝜑) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝜑) |
|
Theorem | necon3bbii 2282 |
Deduction from equality to inequality. (Contributed by NM,
13-Apr-2007.)
|
⊢ (𝜑 ↔ 𝐴 = 𝐵) ⇒ ⊢ (¬ 𝜑 ↔ 𝐴 ≠ 𝐵) |
|
Theorem | necon3bii 2283 |
Inference from equality to inequality. (Contributed by NM,
23-Feb-2005.)
|
⊢ (𝐴 = 𝐵 ↔ 𝐶 = 𝐷) ⇒ ⊢ (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷) |
|
Theorem | necon3abid 2284 |
Deduction from equality to inequality. (Contributed by NM,
21-Mar-2007.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓)) |
|
Theorem | necon3bbid 2285 |
Deduction from equality to inequality. (Contributed by NM,
2-Jun-2007.)
|
⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵)) |
|
Theorem | necon3bid 2286 |
Deduction from equality to inequality. (Contributed by NM,
23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
|
Theorem | necon3ad 2287 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓)) |
|
Theorem | necon3bd 2288 |
Contrapositive law deduction for inequality. (Contributed by NM,
2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵)) |
|
Theorem | necon3d 2289 |
Contrapositive law deduction for inequality. (Contributed by NM,
10-Jun-2006.)
|
⊢ (𝜑 → (𝐴 = 𝐵 → 𝐶 = 𝐷)) ⇒ ⊢ (𝜑 → (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵)) |
|
Theorem | nesym 2290 |
Characterization of inequality in terms of reversed equality (see
bicom 138). (Contributed by BJ, 7-Jul-2018.)
|
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐵 = 𝐴) |
|
Theorem | nesymi 2291 |
Inference associated with nesym 2290. (Contributed by BJ, 7-Jul-2018.)
|
⊢ 𝐴 ≠ 𝐵 ⇒ ⊢ ¬ 𝐵 = 𝐴 |
|
Theorem | nesymir 2292 |
Inference associated with nesym 2290. (Contributed by BJ, 7-Jul-2018.)
|
⊢ ¬ 𝐴 = 𝐵 ⇒ ⊢ 𝐵 ≠ 𝐴 |
|
Theorem | necon3i 2293 |
Contrapositive inference for inequality. (Contributed by NM,
9-Aug-2006.)
|
⊢ (𝐴 = 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵) |
|
Theorem | necon3ai 2294 |
Contrapositive inference for inequality. (Contributed by NM,
23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝐴 ≠ 𝐵 → ¬ 𝜑) |
|
Theorem | necon3bi 2295 |
Contrapositive inference for inequality. (Contributed by NM,
1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
|
⊢ (𝐴 = 𝐵 → 𝜑) ⇒ ⊢ (¬ 𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon1aidc 2296 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 → 𝐴 = 𝐵)) ⇒ ⊢ (DECID 𝜑 → (𝐴 ≠ 𝐵 → 𝜑)) |
|
Theorem | necon1bidc 2297 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
⊢ (DECID 𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → 𝜑)) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (¬ 𝜑 → 𝐴 = 𝐵)) |
|
Theorem | necon1idc 2298 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
⊢ (𝐴 ≠ 𝐵 → 𝐶 = 𝐷) ⇒ ⊢ (DECID 𝐴 = 𝐵 → (𝐶 ≠ 𝐷 → 𝐴 = 𝐵)) |
|
Theorem | necon2ai 2299 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
⊢ (𝐴 = 𝐵 → ¬ 𝜑) ⇒ ⊢ (𝜑 → 𝐴 ≠ 𝐵) |
|
Theorem | necon2bi 2300 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝐴 = 𝐵 → ¬ 𝜑) |