Theorem List for Intuitionistic Logic Explorer - 2301-2400 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | necon1bidc 2301 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
15-May-2018.)
|
DECID    DECID 
   |
|
Theorem | necon1idc 2302 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
  DECID
    |
|
Theorem | necon2ai 2303 |
Contrapositive inference for inequality. (Contributed by NM,
16-Jan-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
     |
|
Theorem | necon2bi 2304 |
Contrapositive inference for inequality. (Contributed by NM,
1-Apr-2007.)
|
     |
|
Theorem | necon2i 2305 |
Contrapositive inference for inequality. (Contributed by NM,
18-Mar-2007.)
|
  
  |
|
Theorem | necon2ad 2306 |
Contrapositive inference for inequality. (Contributed by NM,
19-Apr-2007.) (Proof rewritten by Jim Kingdon, 16-May-2018.)
|
 
   
   |
|
Theorem | necon2bd 2307 |
Contrapositive inference for inequality. (Contributed by NM,
13-Apr-2007.)
|
     
   |
|
Theorem | necon2d 2308 |
Contrapositive inference for inequality. (Contributed by NM,
28-Dec-2008.)
|
 
  

   |
|
Theorem | necon1abiidc 2309 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID     |
|
Theorem | necon1bbiidc 2310 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID 
   |
|
Theorem | necon1abiddc 2311 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
 DECID 
    DECID      |
|
Theorem | necon1bbiddc 2312 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
 DECID
    
DECID
     |
|
Theorem | necon2abiidc 2313 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID 
   |
|
Theorem | necon2bbii 2314 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID     |
|
Theorem | necon2abiddc 2315 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
 DECID     
DECID

    |
|
Theorem | necon2bbiddc 2316 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
 DECID
     DECID
     |
|
Theorem | necon4aidc 2317 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID     |
|
Theorem | necon4idc 2318 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
16-May-2018.)
|
DECID    DECID
    |
|
Theorem | necon4addc 2319 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
 DECID
     DECID      |
|
Theorem | necon4bddc 2320 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
 DECID      DECID      |
|
Theorem | necon4ddc 2321 |
Contrapositive inference for inequality. (Contributed by Jim Kingdon,
17-May-2018.)
|
 DECID
    
DECID
     |
|
Theorem | necon4abiddc 2322 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 18-May-2018.)
|
 DECID
DECID       DECID
DECID       |
|
Theorem | necon4bbiddc 2323 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
 DECID DECID 
     DECID DECID 
     |
|
Theorem | necon4biddc 2324 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
 DECID
DECID       DECID
DECID       |
|
Theorem | necon1addc 2325 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
 DECID      DECID      |
|
Theorem | necon1bddc 2326 |
Contrapositive deduction for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
 DECID
     DECID
     |
|
Theorem | necon1ddc 2327 |
Contrapositive law deduction for inequality. (Contributed by Jim
Kingdon, 19-May-2018.)
|
 DECID
    
DECID
     |
|
Theorem | neneqad 2328 |
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.)
|
     |
|
Theorem | nebidc 2329 |
Contraposition law for inequality. (Contributed by Jim Kingdon,
19-May-2018.)
|
DECID DECID          |
|
Theorem | pm13.18 2330 |
Theorem *13.18 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
     |
|
Theorem | pm13.181 2331 |
Theorem *13.181 in [WhiteheadRussell]
p. 178. (Contributed by Andrew
Salmon, 3-Jun-2011.)
|
     |
|
Theorem | pm2.21ddne 2332 |
A contradiction implies anything. Equality/inequality deduction form.
(Contributed by David Moews, 28-Feb-2017.)
|
       |
|
Theorem | necom 2333 |
Commutation of inequality. (Contributed by NM, 14-May-1999.)
|
   |
|
Theorem | necomi 2334 |
Inference from commutative law for inequality. (Contributed by NM,
17-Oct-2012.)
|
 |
|
Theorem | necomd 2335 |
Deduction from commutative law for inequality. (Contributed by NM,
12-Feb-2008.)
|
     |
|
Theorem | neanior 2336 |
A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.)
|
       |
|
Theorem | ne3anior 2337 |
A De Morgan's law for inequality. (Contributed by NM, 30-Sep-2013.)
(Proof rewritten by Jim Kingdon, 19-May-2018.)
|
   
   |
|
Theorem | nemtbir 2338 |
An inference from an inequality, related to modus tollens. (Contributed
by NM, 13-Apr-2007.)
|
   |
|
Theorem | nelne1 2339 |
Two classes are different if they don't contain the same element.
(Contributed by NM, 3-Feb-2012.)
|
  
  |
|
Theorem | nelne2 2340 |
Two classes are different if they don't belong to the same class.
(Contributed by NM, 25-Jun-2012.)
|
  
  |
|
Theorem | nelelne 2341 |
Two classes are different if they don't belong to the same class.
(Contributed by Rodolfo Medina, 17-Oct-2010.) (Proof shortened by AV,
10-May-2020.)
|
     |
|
Theorem | nfne 2342 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
      |
|
Theorem | nfned 2343 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
            |
|
2.1.4.2 Negated membership
|
|
Syntax | wnel 2344 |
Extend wff notation to include negated membership.
|
 |
|
Definition | df-nel 2345 |
Define negated membership. (Contributed by NM, 7-Aug-1994.)
|
   |
|
Theorem | neli 2346 |
Inference associated with df-nel 2345. (Contributed by BJ,
7-Jul-2018.)
|
 |
|
Theorem | nelir 2347 |
Inference associated with df-nel 2345. (Contributed by BJ,
7-Jul-2018.)
|
 |
|
Theorem | neleq1 2348 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
     |
|
Theorem | neleq2 2349 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
     |
|
Theorem | neleq12d 2350 |
Equality theorem for negated membership. (Contributed by FL,
10-Aug-2016.)
|
     
   |
|
Theorem | nfnel 2351 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
      |
|
Theorem | nfneld 2352 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
            |
|
2.1.5 Restricted quantification
|
|
Syntax | wral 2353 |
Extend wff notation to include restricted universal quantification.
|
  |
|
Syntax | wrex 2354 |
Extend wff notation to include restricted existential quantification.
|
  |
|
Syntax | wreu 2355 |
Extend wff notation to include restricted existential uniqueness.
|
  |
|
Syntax | wrmo 2356 |
Extend wff notation to include restricted "at most one."
|
  |
|
Syntax | crab 2357 |
Extend class notation to include the restricted class abstraction (class
builder).
|

  |
|
Definition | df-ral 2358 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19-Aug-1993.)
|
 
      |
|
Definition | df-rex 2359 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30-Aug-1993.)
|
 
      |
|
Definition | df-reu 2360 |
Define restricted existential uniqueness. (Contributed by NM,
22-Nov-1994.)
|
 
      |
|
Definition | df-rmo 2361 |
Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|
 
      |
|
Definition | df-rab 2362 |
Define a restricted class abstraction (class builder), which is the class
of all in such that is true. Definition
of
[TakeutiZaring] p. 20. (Contributed
by NM, 22-Nov-1994.)
|
  
    |
|
Theorem | ralnex 2363 |
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21-Jan-1997.)
|
     |
|
Theorem | rexnalim 2364 |
Relationship between restricted universal and existential quantifiers. In
classical logic this would be a biconditional. (Contributed by Jim
Kingdon, 17-Aug-2018.)
|
     |
|
Theorem | ralexim 2365 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
 

  |
|
Theorem | rexalim 2366 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
 

  |
|
Theorem | ralbida 2367 |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 6-Oct-2003.)
|
               |
|
Theorem | rexbida 2368 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 6-Oct-2003.)
|
               |
|
Theorem | ralbidva 2369* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 4-Mar-1997.)
|
             |
|
Theorem | rexbidva 2370* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 9-Mar-1997.)
|
             |
|
Theorem | ralbid 2371 |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 27-Jun-1998.)
|
             |
|
Theorem | rexbid 2372 |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 27-Jun-1998.)
|
             |
|
Theorem | ralbidv 2373* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 20-Nov-1994.)
|
           |
|
Theorem | rexbidv 2374* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 20-Nov-1994.)
|
           |
|
Theorem | ralbidv2 2375* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 6-Apr-1997.)
|
    
     
    |
|
Theorem | rexbidv2 2376* |
Formula-building rule for restricted existential quantifier (deduction
rule). (Contributed by NM, 22-May-1999.)
|
          
    |
|
Theorem | ralbii 2377 |
Inference adding restricted universal quantifier to both sides of an
equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario
Carneiro, 17-Oct-2016.)
|
   
   |
|
Theorem | rexbii 2378 |
Inference adding restricted existential quantifier to both sides of an
equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario
Carneiro, 17-Oct-2016.)
|
   
   |
|
Theorem | 2ralbii 2379 |
Inference adding two restricted universal quantifiers to both sides of
an equivalence. (Contributed by NM, 1-Aug-2004.)
|
    
    |
|
Theorem | 2rexbii 2380 |
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 11-Nov-1995.)
|
    
 
  |
|
Theorem | ralbii2 2381 |
Inference adding different restricted universal quantifiers to each side
of an equivalence. (Contributed by NM, 15-Aug-2005.)
|
 
 
   
   |
|
Theorem | rexbii2 2382 |
Inference adding different restricted existential quantifiers to each
side of an equivalence. (Contributed by NM, 4-Feb-2004.)
|
       
   |
|
Theorem | raleqbii 2383 |
Equality deduction for restricted universal quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1-May-2017.)
|
       |
|
Theorem | rexeqbii 2384 |
Equality deduction for restricted existential quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1-May-2017.)
|
       |
|
Theorem | ralbiia 2385 |
Inference adding restricted universal quantifier to both sides of an
equivalence. (Contributed by NM, 26-Nov-2000.)
|
     
   |
|
Theorem | rexbiia 2386 |
Inference adding restricted existential quantifier to both sides of an
equivalence. (Contributed by NM, 26-Oct-1999.)
|
     
   |
|
Theorem | 2rexbiia 2387* |
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 1-Aug-2004.)
|
        
 
  |
|
Theorem | r2alf 2388* |
Double restricted universal quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
    
          |
|
Theorem | r2exf 2389* |
Double restricted existential quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
    
          |
|
Theorem | r2al 2390* |
Double restricted universal quantification. (Contributed by NM,
19-Nov-1995.)
|
  
          |
|
Theorem | r2ex 2391* |
Double restricted existential quantification. (Contributed by NM,
11-Nov-1995.)
|
  
          |
|
Theorem | 2ralbida 2392* |
Formula-building rule for restricted universal quantifier (deduction
rule). (Contributed by NM, 24-Feb-2004.)
|
     
          
    |
|
Theorem | 2ralbidva 2393* |
Formula-building rule for restricted universal quantifiers (deduction
rule). (Contributed by NM, 4-Mar-1997.)
|
  
 
     
 
    |
|
Theorem | 2rexbidva 2394* |
Formula-building rule for restricted existential quantifiers (deduction
rule). (Contributed by NM, 15-Dec-2004.)
|
  
 
     

 
   |
|
Theorem | 2ralbidv 2395* |
Formula-building rule for restricted universal quantifiers (deduction
rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon
Jaroszewicz, 16-Mar-2007.)
|
        
    |
|
Theorem | 2rexbidv 2396* |
Formula-building rule for restricted existential quantifiers (deduction
rule). (Contributed by NM, 28-Jan-2006.)
|
       
 
   |
|
Theorem | rexralbidv 2397* |
Formula-building rule for restricted quantifiers (deduction rule).
(Contributed by NM, 28-Jan-2006.)
|
        
    |
|
Theorem | ralinexa 2398 |
A transformation of restricted quantifiers and logical connectives.
(Contributed by NM, 4-Sep-2005.)
|
         |
|
Theorem | risset 2399* |
Two ways to say "
belongs to ."
(Contributed by NM,
22-Nov-1994.)
|
    |
|
Theorem | hbral 2400 |
Bound-variable hypothesis builder for restricted quantification.
(Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy,
13-Dec-2009.)
|
        
  
  |