HomeHome Intuitionistic Logic Explorer
Theorem List (p. 23 of 73)
< 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
 
Theoremneeq12i 2201 Inference for inequality. (Contributed by NM, 24-Jul-2012.)
A = B    &   𝐶 = 𝐷       (A𝐶B𝐷)
 
Theoremneeq1d 2202 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
(φA = B)       (φ → (A𝐶B𝐶))
 
Theoremneeq2d 2203 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
(φA = B)       (φ → (𝐶A𝐶B))
 
Theoremneeq12d 2204 Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
(φA = B)    &   (φ𝐶 = 𝐷)       (φ → (A𝐶B𝐷))
 
Theoremneneqd 2205 Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(φAB)       (φ → ¬ A = B)
 
Theoremeqnetri 2206 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
A = B    &   B𝐶       A𝐶
 
Theoremeqnetrd 2207 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(φA = B)    &   (φB𝐶)       (φA𝐶)
 
Theoremeqnetrri 2208 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
A = B    &   A𝐶       B𝐶
 
Theoremeqnetrrd 2209 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(φA = B)    &   (φA𝐶)       (φB𝐶)
 
Theoremneeqtri 2210 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
AB    &   B = 𝐶       A𝐶
 
Theoremneeqtrd 2211 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(φAB)    &   (φB = 𝐶)       (φA𝐶)
 
Theoremneeqtrri 2212 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
AB    &   𝐶 = B       A𝐶
 
Theoremneeqtrrd 2213 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
(φAB)    &   (φ𝐶 = B)       (φA𝐶)
 
Theoremsyl5eqner 2214 B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
B = A    &   (φB𝐶)       (φA𝐶)
 
Theorem3netr3d 2215 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(φAB)    &   (φA = 𝐶)    &   (φB = 𝐷)       (φ𝐶𝐷)
 
Theorem3netr4d 2216 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(φAB)    &   (φ𝐶 = A)    &   (φ𝐷 = B)       (φ𝐶𝐷)
 
Theorem3netr3g 2217 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
(φAB)    &   A = 𝐶    &   B = 𝐷       (φ𝐶𝐷)
 
Theorem3netr4g 2218 Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
(φAB)    &   𝐶 = A    &   𝐷 = B       (φ𝐶𝐷)
 
Theoremnecon3abii 2219 Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
(A = Bφ)       (AB ↔ ¬ φ)
 
Theoremnecon3bbii 2220 Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
(φA = B)       φAB)
 
Theoremnecon3bii 2221 Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
(A = B𝐶 = 𝐷)       (AB𝐶𝐷)
 
Theoremnecon3abid 2222 Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
(φ → (A = Bψ))       (φ → (AB ↔ ¬ ψ))
 
Theoremnecon3bbid 2223 Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
(φ → (ψA = B))       (φ → (¬ ψAB))
 
Theoremnecon3bid 2224 Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(φ → (A = B𝐶 = 𝐷))       (φ → (AB𝐶𝐷))
 
Theoremnecon3ad 2225 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(φ → (ψA = B))       (φ → (AB → ¬ ψ))
 
Theoremnecon3bd 2226 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(φ → (A = Bψ))       (φ → (¬ ψAB))
 
Theoremnecon3d 2227 Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
(φ → (A = B𝐶 = 𝐷))       (φ → (𝐶𝐷AB))
 
Theoremnesym 2228 Characterization of inequality in terms of reversed equality (see bicom 128). (Contributed by BJ, 7-Jul-2018.)
(AB ↔ ¬ B = A)
 
Theoremnesymi 2229 Inference associated with nesym 2228. (Contributed by BJ, 7-Jul-2018.)
AB        ¬ B = A
 
Theoremnesymir 2230 Inference associated with nesym 2228. (Contributed by BJ, 7-Jul-2018.)
¬ A = B       BA
 
Theoremnecon3i 2231 Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
(A = B𝐶 = 𝐷)       (𝐶𝐷AB)
 
Theoremnecon3ai 2232 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(φA = B)       (AB → ¬ φ)
 
Theoremnecon3bi 2233 Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
(A = Bφ)       φAB)
 
Theoremnecon1aidc 2234 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID φ → (¬ φA = B))       (DECID φ → (ABφ))
 
Theoremnecon1bidc 2235 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
(DECID A = B → (ABφ))       (DECID A = B → (¬ φA = B))
 
Theoremnecon1idc 2236 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(AB𝐶 = 𝐷)       (DECID A = B → (𝐶𝐷A = B))
 
Theoremnecon2ai 2237 Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(A = B → ¬ φ)       (φAB)
 
Theoremnecon2bi 2238 Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
(φAB)       (A = B → ¬ φ)
 
Theoremnecon2i 2239 Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
(A = B𝐶𝐷)       (𝐶 = 𝐷AB)
 
Theoremnecon2ad 2240 Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
(φ → (A = B → ¬ ψ))       (φ → (ψAB))
 
Theoremnecon2bd 2241 Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
(φ → (ψAB))       (φ → (A = B → ¬ ψ))
 
Theoremnecon2d 2242 Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
(φ → (A = B𝐶𝐷))       (φ → (𝐶 = 𝐷AB))
 
Theoremnecon1abiidc 2243 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID φ → (¬ φA = B))       (DECID φ → (ABφ))
 
Theoremnecon1bbiidc 2244 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID A = B → (ABφ))       (DECID A = B → (¬ φA = B))
 
Theoremnecon1abiddc 2245 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(φ → (DECID ψ → (¬ ψA = B)))       (φ → (DECID ψ → (ABψ)))
 
Theoremnecon1bbiddc 2246 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(φ → (DECID A = B → (ABψ)))       (φ → (DECID A = B → (¬ ψA = B)))
 
Theoremnecon2abiidc 2247 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID φ → (A = B ↔ ¬ φ))       (DECID φ → (φAB))
 
Theoremnecon2bbii 2248 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID A = B → (φAB))       (DECID A = B → (A = B ↔ ¬ φ))
 
Theoremnecon2abiddc 2249 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(φ → (DECID ψ → (A = B ↔ ¬ ψ)))       (φ → (DECID ψ → (ψAB)))
 
Theoremnecon2bbiddc 2250 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(φ → (DECID A = B → (ψAB)))       (φ → (DECID A = B → (A = B ↔ ¬ ψ)))
 
Theoremnecon4aidc 2251 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID A = B → (AB → ¬ φ))       (DECID A = B → (φA = B))
 
Theoremnecon4idc 2252 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
(DECID A = B → (AB𝐶𝐷))       (DECID A = B → (𝐶 = 𝐷A = B))
 
Theoremnecon4addc 2253 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(φ → (DECID A = B → (AB → ¬ ψ)))       (φ → (DECID A = B → (ψA = B)))
 
Theoremnecon4bddc 2254 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(φ → (DECID ψ → (¬ ψAB)))       (φ → (DECID ψ → (A = Bψ)))
 
Theoremnecon4ddc 2255 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
(φ → (DECID A = B → (AB𝐶𝐷)))       (φ → (DECID A = B → (𝐶 = 𝐷A = B)))
 
Theoremnecon4abiddc 2256 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
(φ → (DECID A = B → (DECID ψ → (AB ↔ ¬ ψ))))       (φ → (DECID A = B → (DECID ψ → (A = Bψ))))
 
Theoremnecon4bbiddc 2257 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(φ → (DECID ψ → (DECID A = B → (¬ ψAB))))       (φ → (DECID ψ → (DECID A = B → (ψA = B))))
 
Theoremnecon4biddc 2258 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (AB𝐶𝐷))))       (φ → (DECID A = B → (DECID 𝐶 = 𝐷 → (A = B𝐶 = 𝐷))))
 
Theoremnecon1addc 2259 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(φ → (DECID ψ → (¬ ψA = B)))       (φ → (DECID ψ → (ABψ)))
 
Theoremnecon1bddc 2260 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(φ → (DECID A = B → (ABψ)))       (φ → (DECID A = B → (¬ ψA = B)))
 
Theoremnecon1ddc 2261 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(φ → (DECID A = B → (AB𝐶 = 𝐷)))       (φ → (DECID A = B → (𝐶𝐷A = B)))
 
Theoremneneqad 2262 If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2205. One-way deduction form of df-ne 2188. (Contributed by David Moews, 28-Feb-2017.)
(φ → ¬ A = B)       (φAB)
 
Theoremnebidc 2263 Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
(DECID A = B → (DECID 𝐶 = 𝐷 → ((A = B𝐶 = 𝐷) ↔ (AB𝐶𝐷))))
 
Theorempm13.18 2264 Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((A = B A𝐶) → B𝐶)
 
Theorempm13.181 2265 Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
((A = B B𝐶) → A𝐶)
 
Theorempm2.21ddne 2266 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
(φA = B)    &   (φAB)       (φψ)
 
Theoremnecom 2267 Commutation of inequality. (Contributed by NM, 14-May-1999.)
(ABBA)
 
Theoremnecomi 2268 Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
AB       BA
 
Theoremnecomd 2269 Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
(φAB)       (φBA)
 
Theoremneanior 2270 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
((AB 𝐶𝐷) ↔ ¬ (A = B 𝐶 = 𝐷))
 
Theoremne3anior 2271 A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
((AB 𝐶𝐷 𝐸𝐹) ↔ ¬ (A = B 𝐶 = 𝐷 𝐸 = 𝐹))
 
Theoremnemtbir 2272 An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
AB    &   (φA = B)        ¬ φ
 
Theoremnelne1 2273 Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
((A B ¬ A 𝐶) → B𝐶)
 
Theoremnelne2 2274 Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
((A 𝐶 ¬ B 𝐶) → AB)
 
Theoremnfne 2275 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
xA    &   xB       x AB
 
Theoremnfned 2276 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
(φxA)    &   (φxB)       (φ → Ⅎx AB)
 
2.1.4.2  Negated membership
 
Theoremneli 2277 Inference associated with df-nel 2189. (Contributed by BJ, 7-Jul-2018.)
AB        ¬ A B
 
Theoremnelir 2278 Inference associated with df-nel 2189. (Contributed by BJ, 7-Jul-2018.)
¬ A B       AB
 
Theoremneleq1 2279 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(A = B → (A𝐶B𝐶))
 
Theoremneleq2 2280 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
(A = B → (𝐶A𝐶B))
 
Theoremneleq12d 2281 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
(φA = B)    &   (φ𝐶 = 𝐷)       (φ → (A𝐶B𝐷))
 
Theoremnfnel 2282 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
xA    &   xB       x AB
 
Theoremnfneld 2283 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
(φxA)    &   (φxB)       (φ → Ⅎx AB)
 
2.1.5  Restricted quantification
 
Syntaxwral 2284 Extend wff notation to include restricted universal quantification.
wff x A φ
 
Syntaxwrex 2285 Extend wff notation to include restricted existential quantification.
wff x A φ
 
Syntaxwreu 2286 Extend wff notation to include restricted existential uniqueness.
wff ∃!x A φ
 
Syntaxwrmo 2287 Extend wff notation to include restricted "at most one."
wff ∃*x A φ
 
Syntaxcrab 2288 Extend class notation to include the restricted class abstraction (class builder).
class {x Aφ}
 
Definitiondf-ral 2289 Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)
(x A φx(x Aφ))
 
Definitiondf-rex 2290 Define restricted existential quantification. Special case of Definition 4.15(4) of [TakeutiZaring] p. 22. (Contributed by NM, 30-Aug-1993.)
(x A φx(x A φ))
 
Definitiondf-reu 2291 Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.)
(∃!x A φ∃!x(x A φ))
 
Definitiondf-rmo 2292 Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
(∃*x A φ∃*x(x A φ))
 
Definitiondf-rab 2293 Define a restricted class abstraction (class builder), which is the class of all x in A such that φ is true. Definition of [TakeutiZaring] p. 20. (Contributed by NM, 22-Nov-1994.)
{x Aφ} = {x ∣ (x A φ)}
 
Theoremralnex 2294 Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
(x A ¬ φ ↔ ¬ x A φ)
 
Theoremrexnalim 2295 Relationship between restricted universal and existential quantifiers. In classical logic this would be a biconditional. (Contributed by Jim Kingdon, 17-Aug-2018.)
(x A ¬ φ → ¬ x A φ)
 
Theoremralexim 2296 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
(x A φ → ¬ x A ¬ φ)
 
Theoremrexalim 2297 Relationship between restricted universal and existential quantifiers. (Contributed by Jim Kingdon, 17-Aug-2018.)
(x A φ → ¬ x A ¬ φ)
 
Theoremralbida 2298 Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
xφ    &   ((φ x A) → (ψχ))       (φ → (x A ψx A χ))
 
Theoremrexbida 2299 Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 6-Oct-2003.)
xφ    &   ((φ x A) → (ψχ))       (φ → (x A ψx A χ))
 
Theoremralbidva 2300* Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 4-Mar-1997.)
((φ x A) → (ψχ))       (φ → (x A ψx A χ))
    < 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-7215
  Copyright terms: Public domain < Previous  Next >