HomeHome Intuitionistic Logic Explorer
Theorem List (p. 23 of 95)
< Previous  Next >
Browser slow? Try the
Unicode 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
 
2.1.4  Negated equality and membership
 
Syntaxwne 2201 Extend wff notation to include inequality.
 =/=
 
Syntaxwnel 2202 Extend wff notation to include negated membership.
 e/
 
Definitiondf-ne 2203 Define inequality. (Contributed by NM, 5-Aug-1993.)
 =/=
 
Definitiondf-nel 2204 Define negated membership. (Contributed by NM, 7-Aug-1994.)
 e/
 
2.1.4.1  Negated equality
 
Theoremneii 2205 Inference associated with df-ne 2203. (Contributed by BJ, 7-Jul-2018.)
 =/=    =>   
 
Theoremneir 2206 Inference associated with df-ne 2203. (Contributed by BJ, 7-Jul-2018.)
   =>     =/=
 
Theoremnner 2207 Negation of inequality. (Contributed by Jim Kingdon, 23-Dec-2018.)
 =/=
 
Theoremnnedc 2208 Negation of inequality where equality is decidable. (Contributed by Jim Kingdon, 15-May-2018.)
DECID  =/=
 
Theoremdcned 2209 Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.)
DECID    =>    DECID  =/=
 
Theoremneirr 2210 No class is unequal to itself. (Contributed by Stefan O'Rear, 1-Jan-2015.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
 =/=
 
Theoremdcne 2211 Decidable equality expressed in terms of  =/=. Basically the same as df-dc 742. (Contributed by Jim Kingdon, 14-Mar-2020.)
DECID  =/=
 
Theoremnonconne 2212 Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012.)
 =/=
 
Theoremneeq1 2213 Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
 =/=  C  =/=  C
 
Theoremneeq2 2214 Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)
 C  =/=  C  =/=
 
Theoremneeq1i 2215 Inference for inequality. (Contributed by NM, 29-Apr-2005.)
   =>     =/=  C  =/=  C
 
Theoremneeq2i 2216 Inference for inequality. (Contributed by NM, 29-Apr-2005.)
   =>     C  =/=  C  =/=
 
Theoremneeq12i 2217 Inference for inequality. (Contributed by NM, 24-Jul-2012.)
   &     C  D   =>     =/=  C  =/=  D
 
Theoremneeq1d 2218 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
   =>     =/=  C  =/=  C
 
Theoremneeq2d 2219 Deduction for inequality. (Contributed by NM, 25-Oct-1999.)
   =>     C  =/=  C  =/=
 
Theoremneeq12d 2220 Deduction for inequality. (Contributed by NM, 24-Jul-2012.)
   &     C  D   =>     =/=  C  =/=  D
 
Theoremneneqd 2221 Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
 =/=    =>   
 
Theoremeqnetri 2222 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
   &     =/=  C   =>     =/=  C
 
Theoremeqnetrd 2223 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
   &     =/=  C   =>     =/=  C
 
Theoremeqnetrri 2224 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
   &     =/=  C   =>     =/=  C
 
Theoremeqnetrrd 2225 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
   &     =/=  C   =>     =/=  C
 
Theoremneeqtri 2226 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
 =/=    &     C   =>     =/=  C
 
Theoremneeqtrd 2227 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
 =/=    &     C   =>     =/=  C
 
Theoremneeqtrri 2228 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
 =/=    &     C    =>     =/=  C
 
Theoremneeqtrrd 2229 Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)
 =/=    &     C    =>     =/=  C
 
Theoremsyl5eqner 2230 B chained equality inference for inequality. (Contributed by NM, 6-Jun-2012.)
   &     =/=  C   =>     =/=  C
 
Theorem3netr3d 2231 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
 =/=    &     C   &     D   =>     C  =/=  D
 
Theorem3netr4d 2232 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
 =/=    &     C    &     D    =>     C  =/=  D
 
Theorem3netr3g 2233 Substitution of equality into both sides of an inequality. (Contributed by NM, 24-Jul-2012.)
 =/=    &     C   &     D   =>     C  =/=  D
 
Theorem3netr4g 2234 Substitution of equality into both sides of an inequality. (Contributed by NM, 14-Jun-2012.)
 =/=    &     C    &     D    =>     C  =/=  D
 
Theoremnecon3abii 2235 Deduction from equality to inequality. (Contributed by NM, 9-Nov-2007.)
   =>     =/=
 
Theoremnecon3bbii 2236 Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
   =>     =/=
 
Theoremnecon3bii 2237 Inference from equality to inequality. (Contributed by NM, 23-Feb-2005.)
 C  D   =>     =/=  C  =/=  D
 
Theoremnecon3abid 2238 Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
   =>     =/=
 
Theoremnecon3bbid 2239 Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
   =>     =/=
 
Theoremnecon3bid 2240 Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 C  D   =>     =/=  C  =/=  D
 
Theoremnecon3ad 2241 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
   =>     =/=
 
Theoremnecon3bd 2242 Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
   =>     =/=
 
Theoremnecon3d 2243 Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
 C  D   =>     C  =/=  D  =/=
 
Theoremnesym 2244 Characterization of inequality in terms of reversed equality (see bicom 128). (Contributed by BJ, 7-Jul-2018.)
 =/=
 
Theoremnesymi 2245 Inference associated with nesym 2244. (Contributed by BJ, 7-Jul-2018.)
 =/=    =>   
 
Theoremnesymir 2246 Inference associated with nesym 2244. (Contributed by BJ, 7-Jul-2018.)
   =>     =/=
 
Theoremnecon3i 2247 Contrapositive inference for inequality. (Contributed by NM, 9-Aug-2006.)
 C  D   =>     C  =/=  D  =/=
 
Theoremnecon3ai 2248 Contrapositive inference for inequality. (Contributed by NM, 23-May-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
   =>     =/=
 
Theoremnecon3bi 2249 Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
   =>     =/=
 
Theoremnecon1aidc 2250 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon1bidc 2251 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 15-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon1idc 2252 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
 =/=  C  D   =>    DECID  C  =/=  D
 
Theoremnecon2ai 2253 Contrapositive inference for inequality. (Contributed by NM, 16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
   =>     =/=
 
Theoremnecon2bi 2254 Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
 =/=    =>   
 
Theoremnecon2i 2255 Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.)
 C  =/=  D   =>     C  D  =/=
 
Theoremnecon2ad 2256 Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
   =>     =/=
 
Theoremnecon2bd 2257 Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
 =/=    =>   
 
Theoremnecon2d 2258 Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)
 C  =/=  D   =>     C  D  =/=
 
Theoremnecon1abiidc 2259 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon1bbiidc 2260 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon1abiddc 2261 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon1bbiddc 2262 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon2abiidc 2263 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon2bbii 2264 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon2abiddc 2265 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon2bbiddc 2266 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon4aidc 2267 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon4idc 2268 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 16-May-2018.)
DECID  =/=  C  =/=  D   =>    DECID  C  D
 
Theoremnecon4addc 2269 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon4bddc 2270 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon4ddc 2271 Contrapositive inference for inequality. (Contributed by Jim Kingdon, 17-May-2018.)
DECID  =/=  C  =/=  D   =>    DECID  C  D
 
Theoremnecon4abiddc 2272 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 18-May-2018.)
DECID DECID  =/=    =>    DECID DECID
 
Theoremnecon4bbiddc 2273 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID DECID  =/=    =>    DECID DECID
 
Theoremnecon4biddc 2274 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID DECID  C  D  =/=  C  =/=  D   =>    DECID DECID  C  D  C  D
 
Theoremnecon1addc 2275 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID    =>    DECID  =/=
 
Theoremnecon1bddc 2276 Contrapositive deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID  =/=    =>    DECID
 
Theoremnecon1ddc 2277 Contrapositive law deduction for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID  =/=  C  D   =>    DECID  C  =/=  D
 
Theoremneneqad 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.)
   =>     =/=
 
Theoremnebidc 2279 Contraposition law for inequality. (Contributed by Jim Kingdon, 19-May-2018.)
DECID DECID  C  D  C  D  =/=  C  =/=  D
 
Theorempm13.18 2280 Theorem *13.18 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
 =/=  C  =/=  C
 
Theorempm13.181 2281 Theorem *13.181 in [WhiteheadRussell] p. 178. (Contributed by Andrew Salmon, 3-Jun-2011.)
 =/=  C  =/=  C
 
Theorempm2.21ddne 2282 A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.)
   &     =/=    =>   
 
Theoremnecom 2283 Commutation of inequality. (Contributed by NM, 14-May-1999.)
 =/=  =/=
 
Theoremnecomi 2284 Inference from commutative law for inequality. (Contributed by NM, 17-Oct-2012.)
 =/=    =>     =/=
 
Theoremnecomd 2285 Deduction from commutative law for inequality. (Contributed by NM, 12-Feb-2008.)
 =/=    =>     =/=
 
Theoremneanior 2286 A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
 =/=  C  =/=  D  C  D
 
Theoremne3anior 2287 A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.) (Proof rewritten by Jim Kingdon, 19-May-2018.)
 =/=  C  =/=  D  E  =/=  F  C  D  E  F
 
Theoremnemtbir 2288 An inference from an inequality, related to modus tollens. (Contributed by NM, 13-Apr-2007.)
 =/=    &       =>   
 
Theoremnelne1 2289 Two classes are different if they don't contain the same element. (Contributed by NM, 3-Feb-2012.)
 C  =/=  C
 
Theoremnelne2 2290 Two classes are different if they don't belong to the same class. (Contributed by NM, 25-Jun-2012.)
 C  C  =/=
 
Theoremnfne 2291 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/  =/=
 
Theoremnfned 2292 Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/  =/=
 
2.1.4.2  Negated membership
 
Theoremneli 2293 Inference associated with df-nel 2204. (Contributed by BJ, 7-Jul-2018.)
 e/    =>   
 
Theoremnelir 2294 Inference associated with df-nel 2204. (Contributed by BJ, 7-Jul-2018.)
   =>     e/
 
Theoremneleq1 2295 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
 e/  C  e/  C
 
Theoremneleq2 2296 Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994.)
 C  e/  C  e/
 
Theoremneleq12d 2297 Equality theorem for negated membership. (Contributed by FL, 10-Aug-2016.)
   &     C  D   =>     e/  C  e/  D
 
Theoremnfnel 2298 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/  e/
 
Theoremnfneld 2299 Bound-variable hypothesis builder for negated membership. (Contributed by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro, 7-Oct-2016.)
 F/_   &     F/_   =>     F/  e/
 
2.1.5  Restricted quantification
 
Syntaxwral 2300 Extend wff notation to include restricted universal quantification.
    < 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-9457
  Copyright terms: Public domain < Previous  Next >