Theorem List for Intuitionistic Logic Explorer - 2401-2500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nfne 2401 |
Bound-variable hypothesis builder for inequality. (Contributed by NM,
10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.)
|
|
|
Theorem | nfned 2402 |
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 2403 |
Extend wff notation to include negated membership.
|
|
|
Definition | df-nel 2404 |
Define negated membership. (Contributed by NM, 7-Aug-1994.)
|
|
|
Theorem | neli 2405 |
Inference associated with df-nel 2404. (Contributed by BJ,
7-Jul-2018.)
|
|
|
Theorem | nelir 2406 |
Inference associated with df-nel 2404. (Contributed by BJ,
7-Jul-2018.)
|
|
|
Theorem | neleq1 2407 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
|
|
Theorem | neleq2 2408 |
Equality theorem for negated membership. (Contributed by NM,
20-Nov-1994.)
|
|
|
Theorem | neleq12d 2409 |
Equality theorem for negated membership. (Contributed by FL,
10-Aug-2016.)
|
|
|
Theorem | nfnel 2410 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
|
|
Theorem | nfneld 2411 |
Bound-variable hypothesis builder for negated membership. (Contributed
by David Abernethy, 26-Jun-2011.) (Revised by Mario Carneiro,
7-Oct-2016.)
|
|
|
Theorem | elnelne1 2412 |
Two classes are different if they don't contain the same element.
(Contributed by AV, 28-Jan-2020.)
|
|
|
Theorem | elnelne2 2413 |
Two classes are different if they don't belong to the same class.
(Contributed by AV, 28-Jan-2020.)
|
|
|
Theorem | nelcon3d 2414 |
Contrapositive law deduction for negated membership. (Contributed by
AV, 28-Jan-2020.)
|
|
|
Theorem | elnelall 2415 |
A contradiction concerning membership implies anything. (Contributed by
Alexander van der Vekens, 25-Jan-2018.)
|
|
|
2.1.5 Restricted quantification
|
|
Syntax | wral 2416 |
Extend wff notation to include restricted universal quantification.
|
|
|
Syntax | wrex 2417 |
Extend wff notation to include restricted existential quantification.
|
|
|
Syntax | wreu 2418 |
Extend wff notation to include restricted existential uniqueness.
|
|
|
Syntax | wrmo 2419 |
Extend wff notation to include restricted "at most one."
|
|
|
Syntax | crab 2420 |
Extend class notation to include the restricted class abstraction (class
builder).
|
|
|
Definition | df-ral 2421 |
Define restricted universal quantification. Special case of Definition
4.15(3) of [TakeutiZaring] p. 22.
(Contributed by NM, 19-Aug-1993.)
|
|
|
Definition | df-rex 2422 |
Define restricted existential quantification. Special case of Definition
4.15(4) of [TakeutiZaring] p. 22.
(Contributed by NM, 30-Aug-1993.)
|
|
|
Definition | df-reu 2423 |
Define restricted existential uniqueness. (Contributed by NM,
22-Nov-1994.)
|
|
|
Definition | df-rmo 2424 |
Define restricted "at most one". (Contributed by NM, 16-Jun-2017.)
|
|
|
Definition | df-rab 2425 |
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 2426 |
Relationship between restricted universal and existential quantifiers.
(Contributed by NM, 21-Jan-1997.)
|
|
|
Theorem | rexnalim 2427 |
Relationship between restricted universal and existential quantifiers. In
classical logic this would be a biconditional. (Contributed by Jim
Kingdon, 17-Aug-2018.)
|
|
|
Theorem | dfrex2dc 2428 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 29-Jun-2022.)
|
DECID
|
|
Theorem | ralexim 2429 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
|
|
Theorem | rexalim 2430 |
Relationship between restricted universal and existential quantifiers.
(Contributed by Jim Kingdon, 17-Aug-2018.)
|
|
|
Theorem | ralbida 2431 |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 6-Oct-2003.)
|
|
|
Theorem | rexbida 2432 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 6-Oct-2003.)
|
|
|
Theorem | ralbidva 2433* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 4-Mar-1997.)
|
|
|
Theorem | rexbidva 2434* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 9-Mar-1997.)
|
|
|
Theorem | ralbid 2435 |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 27-Jun-1998.)
|
|
|
Theorem | rexbid 2436 |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 27-Jun-1998.)
|
|
|
Theorem | ralbidv 2437* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 20-Nov-1994.)
|
|
|
Theorem | rexbidv 2438* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 20-Nov-1994.)
|
|
|
Theorem | ralbidv2 2439* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 6-Apr-1997.)
|
|
|
Theorem | rexbidv2 2440* |
Formula-building rule for restricted existential quantifier (deduction
form). (Contributed by NM, 22-May-1999.)
|
|
|
Theorem | ralbii 2441 |
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 2442 |
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 2443 |
Inference adding two restricted universal quantifiers to both sides of
an equivalence. (Contributed by NM, 1-Aug-2004.)
|
|
|
Theorem | 2rexbii 2444 |
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 11-Nov-1995.)
|
|
|
Theorem | ralbii2 2445 |
Inference adding different restricted universal quantifiers to each side
of an equivalence. (Contributed by NM, 15-Aug-2005.)
|
|
|
Theorem | rexbii2 2446 |
Inference adding different restricted existential quantifiers to each
side of an equivalence. (Contributed by NM, 4-Feb-2004.)
|
|
|
Theorem | raleqbii 2447 |
Equality deduction for restricted universal quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1-May-2017.)
|
|
|
Theorem | rexeqbii 2448 |
Equality deduction for restricted existential quantifier, changing both
formula and quantifier domain. Inference form. (Contributed by David
Moews, 1-May-2017.)
|
|
|
Theorem | ralbiia 2449 |
Inference adding restricted universal quantifier to both sides of an
equivalence. (Contributed by NM, 26-Nov-2000.)
|
|
|
Theorem | rexbiia 2450 |
Inference adding restricted existential quantifier to both sides of an
equivalence. (Contributed by NM, 26-Oct-1999.)
|
|
|
Theorem | 2rexbiia 2451* |
Inference adding two restricted existential quantifiers to both sides of
an equivalence. (Contributed by NM, 1-Aug-2004.)
|
|
|
Theorem | r2alf 2452* |
Double restricted universal quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
|
|
Theorem | r2exf 2453* |
Double restricted existential quantification. (Contributed by Mario
Carneiro, 14-Oct-2016.)
|
|
|
Theorem | r2al 2454* |
Double restricted universal quantification. (Contributed by NM,
19-Nov-1995.)
|
|
|
Theorem | r2ex 2455* |
Double restricted existential quantification. (Contributed by NM,
11-Nov-1995.)
|
|
|
Theorem | 2ralbida 2456* |
Formula-building rule for restricted universal quantifier (deduction
form). (Contributed by NM, 24-Feb-2004.)
|
|
|
Theorem | 2ralbidva 2457* |
Formula-building rule for restricted universal quantifiers (deduction
form). (Contributed by NM, 4-Mar-1997.)
|
|
|
Theorem | 2rexbidva 2458* |
Formula-building rule for restricted existential quantifiers (deduction
form). (Contributed by NM, 15-Dec-2004.)
|
|
|
Theorem | 2ralbidv 2459* |
Formula-building rule for restricted universal quantifiers (deduction
form). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon
Jaroszewicz, 16-Mar-2007.)
|
|
|
Theorem | 2rexbidv 2460* |
Formula-building rule for restricted existential quantifiers (deduction
form). (Contributed by NM, 28-Jan-2006.)
|
|
|
Theorem | rexralbidv 2461* |
Formula-building rule for restricted quantifiers (deduction form).
(Contributed by NM, 28-Jan-2006.)
|
|
|
Theorem | ralinexa 2462 |
A transformation of restricted quantifiers and logical connectives.
(Contributed by NM, 4-Sep-2005.)
|
|
|
Theorem | risset 2463* |
Two ways to say "
belongs to ."
(Contributed by NM,
22-Nov-1994.)
|
|
|
Theorem | hbral 2464 |
Bound-variable hypothesis builder for restricted quantification.
(Contributed by NM, 1-Sep-1999.) (Revised by David Abernethy,
13-Dec-2009.)
|
|
|
Theorem | hbra1 2465 |
is not free in .
(Contributed by NM,
18-Oct-1996.)
|
|
|
Theorem | nfra1 2466 |
is not free in .
(Contributed by NM, 18-Oct-1996.)
(Revised by Mario Carneiro, 7-Oct-2016.)
|
|
|
Theorem | nfraldxy 2467* |
Not-free for restricted universal quantification where and
are distinct. See nfraldya 2469 for a version with and
distinct instead. (Contributed by Jim Kingdon, 29-May-2018.)
|
|
|
Theorem | nfrexdxy 2468* |
Not-free for restricted existential quantification where and
are distinct. See nfrexdya 2470 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
|
|
Theorem | nfraldya 2469* |
Not-free for restricted universal quantification where and
are distinct. See nfraldxy 2467 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
|
|
Theorem | nfrexdya 2470* |
Not-free for restricted existential quantification where and
are distinct. See nfrexdxy 2468 for a version with and
distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
|
|
Theorem | nfralxy 2471* |
Not-free for restricted universal quantification where and
are distinct. See nfralya 2473 for a version with and distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
|
|
Theorem | nfrexxy 2472* |
Not-free for restricted existential quantification where and
are distinct. See nfrexya 2474 for a version with and distinct
instead. (Contributed by Jim Kingdon, 30-May-2018.)
|
|
|
Theorem | nfralya 2473* |
Not-free for restricted universal quantification where and
are distinct. See nfralxy 2471 for a version with and distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
|
|
Theorem | nfrexya 2474* |
Not-free for restricted existential quantification where and
are distinct. See nfrexxy 2472 for a version with and distinct
instead. (Contributed by Jim Kingdon, 3-Jun-2018.)
|
|
|
Theorem | nfra2xy 2475* |
Not-free given two restricted quantifiers. (Contributed by Jim Kingdon,
20-Aug-2018.)
|
|
|
Theorem | nfre1 2476 |
is not free in .
(Contributed by NM, 19-Mar-1997.)
(Revised by Mario Carneiro, 7-Oct-2016.)
|
|
|
Theorem | r3al 2477* |
Triple restricted universal quantification. (Contributed by NM,
19-Nov-1995.)
|
|
|
Theorem | alral 2478 |
Universal quantification implies restricted quantification. (Contributed
by NM, 20-Oct-2006.)
|
|
|
Theorem | rexex 2479 |
Restricted existence implies existence. (Contributed by NM,
11-Nov-1995.)
|
|
|
Theorem | rsp 2480 |
Restricted specialization. (Contributed by NM, 17-Oct-1996.)
|
|
|
Theorem | rspe 2481 |
Restricted specialization. (Contributed by NM, 12-Oct-1999.)
|
|
|
Theorem | rsp2 2482 |
Restricted specialization. (Contributed by NM, 11-Feb-1997.)
|
|
|
Theorem | rsp2e 2483 |
Restricted specialization. (Contributed by FL, 4-Jun-2012.)
|
|
|
Theorem | rspec 2484 |
Specialization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
|
|
Theorem | rgen 2485 |
Generalization rule for restricted quantification. (Contributed by NM,
19-Nov-1994.)
|
|
|
Theorem | rgen2a 2486* |
Generalization rule for restricted quantification. Note that and
needn't be
distinct (and illustrates the use of dvelimor 1993).
(Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon,
1-Jun-2018.)
|
|
|
Theorem | rgenw 2487 |
Generalization rule for restricted quantification. (Contributed by NM,
18-Jun-2014.)
|
|
|
Theorem | rgen2w 2488 |
Generalization rule for restricted quantification. Note that and
needn't be
distinct. (Contributed by NM, 18-Jun-2014.)
|
|
|
Theorem | mprg 2489 |
Modus ponens combined with restricted generalization. (Contributed by
NM, 10-Aug-2004.)
|
|
|
Theorem | mprgbir 2490 |
Modus ponens on biconditional combined with restricted generalization.
(Contributed by NM, 21-Mar-2004.)
|
|
|
Theorem | ralim 2491 |
Distribution of restricted quantification over implication. (Contributed
by NM, 9-Feb-1997.)
|
|
|
Theorem | ralimi2 2492 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 22-Feb-2004.)
|
|
|
Theorem | ralimia 2493 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 19-Jul-1996.)
|
|
|
Theorem | ralimiaa 2494 |
Inference quantifying both antecedent and consequent. (Contributed by
NM, 4-Aug-2007.)
|
|
|
Theorem | ralimi 2495 |
Inference quantifying both antecedent and consequent, with strong
hypothesis. (Contributed by NM, 4-Mar-1997.)
|
|
|
Theorem | 2ralimi 2496 |
Inference quantifying both antecedent and consequent two times, with
strong hypothesis. (Contributed by AV, 3-Dec-2021.)
|
|
|
Theorem | ral2imi 2497 |
Inference quantifying antecedent, nested antecedent, and consequent,
with a strong hypothesis. (Contributed by NM, 19-Dec-2006.)
|
|
|
Theorem | ralimdaa 2498 |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-Sep-2003.)
|
|
|
Theorem | ralimdva 2499* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 22-May-1999.)
|
|
|
Theorem | ralimdv 2500* |
Deduction quantifying both antecedent and consequent, based on Theorem
19.20 of [Margaris] p. 90.
(Contributed by NM, 8-Oct-2003.)
|
|