HomeHome Intuitionistic Logic Explorer
Theorem List (p. 23 of 111)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2201-2300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremabbi2dv 2201* Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
(𝜑 → (𝑥𝐴𝜓))       (𝜑𝐴 = {𝑥𝜓})
 
Theoremabbi1dv 2202* Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.)
(𝜑 → (𝜓𝑥𝐴))       (𝜑 → {𝑥𝜓} = 𝐴)
 
Theoremabid2 2203* A simplification of class abstraction. Theorem 5.2 of [Quine] p. 35. (Contributed by NM, 26-Dec-1993.)
{𝑥𝑥𝐴} = 𝐴
 
Theoremsb8ab 2204 Substitution of variable in class abstraction. (Contributed by Jim Kingdon, 27-Sep-2018.)
𝑦𝜑       {𝑥𝜑} = {𝑦 ∣ [𝑦 / 𝑥]𝜑}
 
Theoremcbvab 2205 Rule used to change bound variables, using implicit substitution. (Contributed by Andrew Salmon, 11-Jul-2011.)
𝑦𝜑    &   𝑥𝜓    &   (𝑥 = 𝑦 → (𝜑𝜓))       {𝑥𝜑} = {𝑦𝜓}
 
Theoremcbvabv 2206* Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
(𝑥 = 𝑦 → (𝜑𝜓))       {𝑥𝜑} = {𝑦𝜓}
 
Theoremclelab 2207* Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993.)
(𝐴 ∈ {𝑥𝜑} ↔ ∃𝑥(𝑥 = 𝐴𝜑))
 
Theoremclabel 2208* Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006.)
({𝑥𝜑} ∈ 𝐴 ↔ ∃𝑦(𝑦𝐴 ∧ ∀𝑥(𝑥𝑦𝜑)))
 
Theoremsbab 2209* 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
 
Syntaxwnfc 2210 Extend wff definition to include the not-free predicate for classes.
wff 𝑥𝐴
 
Theoremnfcjust 2211* Justification theorem for df-nfc 2212. (Contributed by Mario Carneiro, 13-Oct-2016.)
(∀𝑦𝑥 𝑦𝐴 ↔ ∀𝑧𝑥 𝑧𝐴)
 
Definitiondf-nfc 2212* 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 1391 for wffs; see that definition for more information. (Contributed by Mario Carneiro, 11-Aug-2016.)
(𝑥𝐴 ↔ ∀𝑦𝑥 𝑦𝐴)
 
Theoremnfci 2213* Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥 𝑦𝐴       𝑥𝐴
 
Theoremnfcii 2214* Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
(𝑦𝐴 → ∀𝑥 𝑦𝐴)       𝑥𝐴
 
Theoremnfcr 2215* Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
(𝑥𝐴 → Ⅎ𝑥 𝑦𝐴)
 
Theoremnfcrii 2216* Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴       (𝑦𝐴 → ∀𝑥 𝑦𝐴)
 
Theoremnfcri 2217* Consequence of the not-free predicate. (Note that unlike nfcr 2215, this does not require 𝑦 and 𝐴 to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴       𝑥 𝑦𝐴
 
Theoremnfcd 2218* Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑦𝜑    &   (𝜑 → Ⅎ𝑥 𝑦𝐴)       (𝜑𝑥𝐴)
 
Theoremnfceqi 2219 Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝐴 = 𝐵       (𝑥𝐴𝑥𝐵)
 
Theoremnfcxfr 2220 A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝐴 = 𝐵    &   𝑥𝐵       𝑥𝐴
 
Theoremnfcxfrd 2221 A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝐴 = 𝐵    &   (𝜑𝑥𝐵)       (𝜑𝑥𝐴)
 
Theoremnfceqdf 2222 An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016.)
𝑥𝜑    &   (𝜑𝐴 = 𝐵)       (𝜑 → (𝑥𝐴𝑥𝐵))
 
Theoremnfcv 2223* If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴
 
Theoremnfcvd 2224* If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)
 
Theoremnfab1 2225 Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥{𝑥𝜑}
 
Theoremnfnfc1 2226 𝑥 is bound in 𝑥𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝑥𝐴
 
Theoremnfab 2227 Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝜑       𝑥{𝑦𝜑}
 
Theoremnfaba1 2228 Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 14-Oct-2016.)
𝑥{𝑦 ∣ ∀𝑥𝜑}
 
Theoremnfnfc 2229 Hypothesis builder for 𝑦𝐴. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴       𝑥𝑦𝐴
 
Theoremnfeq 2230 Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴 = 𝐵
 
Theoremnfel 2231 Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝐴    &   𝑥𝐵       𝑥 𝐴𝐵
 
Theoremnfeq1 2232* Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
𝑥𝐴       𝑥 𝐴 = 𝐵
 
Theoremnfel1 2233* Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
𝑥𝐴       𝑥 𝐴𝐵
 
Theoremnfeq2 2234* Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
𝑥𝐵       𝑥 𝐴 = 𝐵
 
Theoremnfel2 2235* Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
𝑥𝐵       𝑥 𝐴𝐵
 
Theoremnfcrd 2236* Consequence of the not-free predicate. (Contributed by Mario Carneiro, 11-Aug-2016.)
(𝜑𝑥𝐴)       (𝜑 → Ⅎ𝑥 𝑦𝐴)
 
Theoremnfeqd 2237 Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴 = 𝐵)
 
Theoremnfeld 2238 Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
(𝜑𝑥𝐴)    &   (𝜑𝑥𝐵)       (𝜑 → Ⅎ𝑥 𝐴𝐵)
 
Theoremdrnfc1 2239 Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
(∀𝑥 𝑥 = 𝑦𝐴 = 𝐵)       (∀𝑥 𝑥 = 𝑦 → (𝑥𝐴𝑦𝐵))
 
Theoremdrnfc2 2240 Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 8-Oct-2016.)
(∀𝑥 𝑥 = 𝑦𝐴 = 𝐵)       (∀𝑥 𝑥 = 𝑦 → (𝑧𝐴𝑧𝐵))
 
Theoremnfabd 2241 Bound-variable hypothesis builder for a class abstraction. (Contributed by Mario Carneiro, 8-Oct-2016.)
𝑦𝜑    &   (𝜑 → Ⅎ𝑥𝜓)       (𝜑𝑥{𝑦𝜓})
 
Theoremdvelimdc 2242 Deduction form of dvelimc 2243. (Contributed by Mario Carneiro, 8-Oct-2016.)
𝑥𝜑    &   𝑧𝜑    &   (𝜑𝑥𝐴)    &   (𝜑𝑧𝐵)    &   (𝜑 → (𝑧 = 𝑦𝐴 = 𝐵))       (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦𝑥𝐵))
 
Theoremdvelimc 2243 Version of dvelim 1936 for classes. (Contributed by Mario Carneiro, 8-Oct-2016.)
𝑥𝐴    &   𝑧𝐵    &   (𝑧 = 𝑦𝐴 = 𝐵)       (¬ ∀𝑥 𝑥 = 𝑦𝑥𝐵)
 
Theoremnfcvf 2244 If 𝑥 and 𝑦 are distinct, then 𝑥 is not free in 𝑦. (Contributed by Mario Carneiro, 8-Oct-2016.)
(¬ ∀𝑥 𝑥 = 𝑦𝑥𝑦)
 
Theoremnfcvf2 2245 If 𝑥 and 𝑦 are distinct, then 𝑦 is not free in 𝑥. (Contributed by Mario Carneiro, 5-Dec-2016.)
(¬ ∀𝑥 𝑥 = 𝑦𝑦𝑥)
 
Theoremcleqf 2246 Establish equality between classes, using bound-variable hypotheses instead of distinct variable conditions. See also cleqh 2182. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.)
𝑥𝐴    &   𝑥𝐵       (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
 
Theoremabid2f 2247 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.)
𝑥𝐴       {𝑥𝑥𝐴} = 𝐴
 
Theoremsbabel 2248* 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
 
Syntaxwne 2249 Extend wff notation to include inequality.
wff 𝐴𝐵
 
Definitiondf-ne 2250 Define inequality. (Contributed by NM, 5-Aug-1993.)
(𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
 
Theoremneii 2251 Inference associated with df-ne 2250. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐴 = 𝐵
 
Theoremneir 2252 Inference associated with df-ne 2250. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴 = 𝐵       𝐴𝐵
 
Theoremnner 2253 Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
(𝐴 = 𝐵 → ¬ 𝐴𝐵)
 
Theoremnnedc 2254 Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝐴 = 𝐵 → (¬ 𝐴𝐵𝐴 = 𝐵))
 
Theoremdcned 2255 Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
(𝜑DECID 𝐴 = 𝐵)       (𝜑DECID 𝐴𝐵)
 
Theoremneqned 2256 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2270. One-way deduction form of df-ne 2250. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2299. (Revised by Wolf Lammen, 22-Nov-2019.)
(𝜑 → ¬ 𝐴 = 𝐵)       (𝜑𝐴𝐵)
 
Theoremneqne 2257 From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
𝐴 = 𝐵𝐴𝐵)
 
Theoremneirr 2258 No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
¬ 𝐴𝐴
 
Theoremeqneqall 2259 A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
(𝐴 = 𝐵 → (𝐴𝐵𝜑))
 
Theoremdcne 2260 Decidable equality expressed in terms of . Basically the same as df-dc 777. (Contributed by Jim Kingdon, 14-Mar-2020.)
(DECID 𝐴 = 𝐵 ↔ (𝐴 = 𝐵𝐴𝐵))
 
Theoremnonconne 2261 Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
¬ (𝐴 = 𝐵𝐴𝐵)
 
Theoremneeq1 2262 Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
(𝐴 = 𝐵 → (𝐴𝐶𝐵𝐶))
 
Theoremneeq2 2263 Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
(𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
 
Theoremneeq1i 2264 Inference for inequality. (Contributed by NM, 29-Apr-2005.)
𝐴 = 𝐵       (𝐴𝐶𝐵𝐶)
 
Theoremneeq2i 2265 Inference for inequality. (Contributed by NM, 29-Apr-2005.)
𝐴 = 𝐵       (𝐶𝐴𝐶𝐵)
 
Theoremneeq12i 2266 Inference for inequality. (Contributed by NM, 24-Jul-2012.)
𝐴 = 𝐵    &   𝐶 = 𝐷       (𝐴𝐶𝐵𝐷)
 
Theoremneeq1d 2267 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐴𝐶𝐵𝐶))
 
Theoremneeq2d 2268 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
(𝜑𝐴 = 𝐵)       (𝜑 → (𝐶𝐴𝐶𝐵))
 
Theoremneeq12d 2269 Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐶 = 𝐷)       (𝜑 → (𝐴𝐶𝐵𝐷))
 
Theoremneneqd 2270 Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝜑𝐴𝐵)       (𝜑 → ¬ 𝐴 = 𝐵)
 
Theoremneneq 2271 From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
(𝐴𝐵 → ¬ 𝐴 = 𝐵)
 
Theoremeqnetri 2272 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴 = 𝐵    &   𝐵𝐶       𝐴𝐶
 
Theoremeqnetrd 2273 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theoremeqnetrri 2274 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴 = 𝐵    &   𝐴𝐶       𝐵𝐶
 
Theoremeqnetrrd 2275 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴 = 𝐵)    &   (𝜑𝐴𝐶)       (𝜑𝐵𝐶)
 
Theoremneeqtri 2276 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴𝐵    &   𝐵 = 𝐶       𝐴𝐶
 
Theoremneeqtrd 2277 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐵 = 𝐶)       (𝜑𝐴𝐶)
 
Theoremneeqtrri 2278 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
𝐴𝐵    &   𝐶 = 𝐵       𝐴𝐶
 
Theoremneeqtrrd 2279 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐵)       (𝜑𝐴𝐶)
 
Theoremsyl5eqner 2280 B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
𝐵 = 𝐴    &   (𝜑𝐵𝐶)       (𝜑𝐴𝐶)
 
Theorem3netr3d 2281 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐴 = 𝐶)    &   (𝜑𝐵 = 𝐷)       (𝜑𝐶𝐷)
 
Theorem3netr4d 2282 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   (𝜑𝐶 = 𝐴)    &   (𝜑𝐷 = 𝐵)       (𝜑𝐶𝐷)
 
Theorem3netr3g 2283 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(𝜑𝐴𝐵)    &   𝐴 = 𝐶    &   𝐵 = 𝐷       (𝜑𝐶𝐷)
 
Theorem3netr4g 2284 Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
(𝜑𝐴𝐵)    &   𝐶 = 𝐴    &   𝐷 = 𝐵       (𝜑𝐶𝐷)
 
Theoremnecon3abii 2285 Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
(𝐴 = 𝐵𝜑)       (𝐴𝐵 ↔ ¬ 𝜑)
 
Theoremnecon3bbii 2286 Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
(𝜑𝐴 = 𝐵)       𝜑𝐴𝐵)
 
Theoremnecon3bii 2287 Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
(𝐴 = 𝐵𝐶 = 𝐷)       (𝐴𝐵𝐶𝐷)
 
Theoremnecon3abid 2288 Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
(𝜑 → (𝐴 = 𝐵𝜓))       (𝜑 → (𝐴𝐵 ↔ ¬ 𝜓))
 
Theoremnecon3bbid 2289 Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
(𝜑 → (𝜓𝐴 = 𝐵))       (𝜑 → (¬ 𝜓𝐴𝐵))
 
Theoremnecon3bid 2290 Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐴𝐵𝐶𝐷))
 
Theoremnecon3ad 2291 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝜓𝐴 = 𝐵))       (𝜑 → (𝐴𝐵 → ¬ 𝜓))
 
Theoremnecon3bd 2292 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑 → (𝐴 = 𝐵𝜓))       (𝜑 → (¬ 𝜓𝐴𝐵))
 
Theoremnecon3d 2293 Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
(𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))       (𝜑 → (𝐶𝐷𝐴𝐵))
 
Theoremnesym 2294 Characterization of inequality in terms of reversed equality (see bicom 138). (Contributed by BJ, 7-Jul-2018.)
(𝐴𝐵 ↔ ¬ 𝐵 = 𝐴)
 
Theoremnesymi 2295 Inference associated with nesym 2294. (Contributed by BJ, 7-Jul-2018.)
𝐴𝐵        ¬ 𝐵 = 𝐴
 
Theoremnesymir 2296 Inference associated with nesym 2294. (Contributed by BJ, 7-Jul-2018.)
¬ 𝐴 = 𝐵       𝐵𝐴
 
Theoremnecon3i 2297 Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
(𝐴 = 𝐵𝐶 = 𝐷)       (𝐶𝐷𝐴𝐵)
 
Theoremnecon3ai 2298 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝜑𝐴 = 𝐵)       (𝐴𝐵 → ¬ 𝜑)
 
Theoremnecon3bi 2299 Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(𝐴 = 𝐵𝜑)       𝜑𝐴𝐵)
 
Theoremnecon1aidc 2300 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID 𝜑 → (¬ 𝜑𝐴 = 𝐵))       (DECID 𝜑 → (𝐴𝐵𝜑))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11080
  Copyright terms: Public domain < Previous  Next >