Home Intuitionistic Logic ExplorerTheorem List (p. 16 of 106) < 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 - 1501-1600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremexlimi 1501 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜓    &   (𝜑𝜓)       (∃𝑥𝜑𝜓)

Theoremexlimd2 1502 Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1503 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)
(𝜑 → ∀𝑥𝜑)    &   (𝜑 → (𝜒 → ∀𝑥𝜒))    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓𝜒))

Theoremexlimdh 1503 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
(𝜑 → ∀𝑥𝜑)    &   (𝜒 → ∀𝑥𝜒)    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓𝜒))

Theoremexlimd 1504 Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.)
𝑥𝜑    &   𝑥𝜒    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓𝜒))

Theoremexlimiv 1505* Inference from Theorem 19.23 of [Margaris] p. 90.

This inference, along with our many variants is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf.

In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C.

In essence, Rule C states that if we can prove that some element 𝑥 exists satisfying a wff, i.e. 𝑥𝜑(𝑥) where 𝜑(𝑥) has 𝑥 free, then we can use 𝜑( C ) as a hypothesis for the proof where C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier.

We cannot do this in Metamath directly. Instead, we use the original 𝜑 (containing 𝑥) as an antecedent for the main part of the proof. We eventually arrive at (𝜑𝜓) where 𝜓 is the theorem to be proved and does not contain 𝑥. Then we apply exlimiv 1505 to arrive at (∃𝑥𝜑𝜓). Finally, we separately prove 𝑥𝜑 and detach it with modus ponens ax-mp 7 to arrive at the final theorem 𝜓. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

(𝜑𝜓)       (∃𝑥𝜑𝜓)

Theoremexim 1506 Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
(∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Theoremeximi 1507 Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
(𝜑𝜓)       (∃𝑥𝜑 → ∃𝑥𝜓)

Theorem2eximi 1508 Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
(𝜑𝜓)       (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)

Theoremeximii 1509 Inference associated with eximi 1507. (Contributed by BJ, 3-Feb-2018.)
𝑥𝜑    &   (𝜑𝜓)       𝑥𝜓

Theoremalinexa 1510 A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
(∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑𝜓))

Theoremexbi 1511 Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
(∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))

Theoremexbii 1512 Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
(𝜑𝜓)       (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Theorem2exbii 1513 Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
(𝜑𝜓)       (∃𝑥𝑦𝜑 ↔ ∃𝑥𝑦𝜓)

Theorem3exbii 1514 Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
(𝜑𝜓)       (∃𝑥𝑦𝑧𝜑 ↔ ∃𝑥𝑦𝑧𝜓)

Theoremexancom 1515 Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
(∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))

Theoremalrimdd 1516 Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜑    &   (𝜑 → Ⅎ𝑥𝜓)    &   (𝜑 → (𝜓𝜒))       (𝜑 → (𝜓 → ∀𝑥𝜒))

Theoremalrimd 1517 Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜑    &   𝑥𝜓    &   (𝜑 → (𝜓𝜒))       (𝜑 → (𝜓 → ∀𝑥𝜒))

Theoremeximdh 1518 Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
(𝜑 → ∀𝑥𝜑)    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Theoremeximd 1519 Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))

Theoremnexd 1520 Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
(𝜑 → ∀𝑥𝜑)    &   (𝜑 → ¬ 𝜓)       (𝜑 → ¬ ∃𝑥𝜓)

Theoremexbidh 1521 Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
(𝜑 → ∀𝑥𝜑)    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Theoremalbid 1522 Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Theoremexbid 1523 Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)
𝑥𝜑    &   (𝜑 → (𝜓𝜒))       (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒))

Theoremexsimpl 1524 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(∃𝑥(𝜑𝜓) → ∃𝑥𝜑)

Theoremexsimpr 1525 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
(∃𝑥(𝜑𝜓) → ∃𝑥𝜓)

Theoremalexdc 1526 Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1552. (Contributed by Jim Kingdon, 2-Jun-2018.)
(∀𝑥DECID 𝜑 → (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑))

Theorem19.29 1527 Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))

Theorem19.29r 1528 Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑𝜓))

Theorem19.29r2 1529 Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
((∃𝑥𝑦𝜑 ∧ ∀𝑥𝑦𝜓) → ∃𝑥𝑦(𝜑𝜓))

Theorem19.29x 1530 Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
((∃𝑥𝑦𝜑 ∧ ∀𝑥𝑦𝜓) → ∃𝑥𝑦(𝜑𝜓))

Theorem19.35-1 1531 Forward direction of Theorem 19.35 of [Margaris] p. 90. The converse holds for classical logic but not (for all propositions) in intuitionistic logic (Contributed by Mario Carneiro, 2-Feb-2015.)
(∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))

Theorem19.35i 1532 Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
𝑥(𝜑𝜓)       (∀𝑥𝜑 → ∃𝑥𝜓)

Theorem19.25 1533 Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
(∀𝑦𝑥(𝜑𝜓) → (∃𝑦𝑥𝜑 → ∃𝑦𝑥𝜓))

Theorem19.30dc 1534 Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
(DECID𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)))

Theorem19.43 1535 Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
(∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓))

Theorem19.33b2 1536 The antecedent provides a condition implying the converse of 19.33 1389. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1537 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.)
((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))

Theorem19.33bdc 1537 Converse of 19.33 1389 given ¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) and a decidability condition. Compare Theorem 19.33 of [Margaris] p. 90. For a version which does not require a decidability condition, see 19.33b2 1536 (Contributed by Jim Kingdon, 23-Apr-2018.)
(DECID𝑥𝜑 → (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓))))

Theorem19.40 1538 Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
(∃𝑥(𝜑𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))

Theorem19.40-2 1539 Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)
(∃𝑥𝑦(𝜑𝜓) → (∃𝑥𝑦𝜑 ∧ ∃𝑥𝑦𝜓))

Theoremexintrbi 1540 Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
(∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑𝜓)))

Theoremexintr 1541 Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
(∀𝑥(𝜑𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑𝜓)))

Theoremalsyl 1542 Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)
((∀𝑥(𝜑𝜓) ∧ ∀𝑥(𝜓𝜒)) → ∀𝑥(𝜑𝜒))

Theoremhbex 1543 If 𝑥 is not free in 𝜑, it is not free in 𝑦𝜑. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
(𝜑 → ∀𝑥𝜑)       (∃𝑦𝜑 → ∀𝑥𝑦𝜑)

Theoremnfex 1544 If 𝑥 is not free in 𝜑, it is not free in 𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
𝑥𝜑       𝑥𝑦𝜑

Theorem19.2 1545 Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)
(∀𝑥𝜑 → ∃𝑦𝜑)

Theoremi19.24 1546 Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1531, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))       ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑𝜓))

Theoremi19.39 1547 Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1531, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)
((∀𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))       ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))

Theorem19.9ht 1548 A closed version of one direction of 19.9 1551. (Contributed by NM, 5-Aug-1993.)
(∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑𝜑))

Theorem19.9t 1549 A closed version of 19.9 1551. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.)
(Ⅎ𝑥𝜑 → (∃𝑥𝜑𝜑))

Theorem19.9h 1550 A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)
(𝜑 → ∀𝑥𝜑)       (∃𝑥𝜑𝜑)

Theorem19.9 1551 A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
𝑥𝜑       (∃𝑥𝜑𝜑)

Theoremalexim 1552 One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1526. (Contributed by Jim Kingdon, 2-Jul-2018.)
(∀𝑥𝜑 → ¬ ∃𝑥 ¬ 𝜑)

Theoremexnalim 1553 One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
(∃𝑥 ¬ 𝜑 → ¬ ∀𝑥𝜑)

Theoremexanaliim 1554 A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)
(∃𝑥(𝜑 ∧ ¬ 𝜓) → ¬ ∀𝑥(𝜑𝜓))

Theoremalexnim 1555 A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)
(∀𝑥𝑦 ¬ 𝜑 → ¬ ∃𝑥𝑦𝜑)

Theoremax6blem 1556 If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. This theorem doesn't use ax6b 1557 compared to hbnt 1559. (Contributed by GD, 27-Jan-2018.)
(𝜑 → ∀𝑥𝜑)       𝜑 → ∀𝑥 ¬ 𝜑)

Theoremax6b 1557 Quantified Negation. Axiom C5-2 of [Monk2] p. 113.

(Contributed by GD, 27-Jan-2018.)

(¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Theoremhbn1 1558 𝑥 is not free in ¬ ∀𝑥𝜑. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
(¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)

Theoremhbnt 1559 Closed theorem version of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
(∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))

Theoremhbn 1560 If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 5-Aug-1993.)
(𝜑 → ∀𝑥𝜑)       𝜑 → ∀𝑥 ¬ 𝜑)

Theoremhbnd 1561 Deduction form of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 3-Jan-2002.)
(𝜑 → ∀𝑥𝜑)    &   (𝜑 → (𝜓 → ∀𝑥𝜓))       (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓))

Theoremnfnt 1562 If 𝑥 is not free in 𝜑, then it is not free in ¬ 𝜑. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)
(Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)

Theoremnfnd 1563 Deduction associated with nfnt 1562. (Contributed by Mario Carneiro, 24-Sep-2016.)
(𝜑 → Ⅎ𝑥𝜓)       (𝜑 → Ⅎ𝑥 ¬ 𝜓)

Theoremnfn 1564 Inference associated with nfnt 1562. (Contributed by Mario Carneiro, 11-Aug-2016.)
𝑥𝜑       𝑥 ¬ 𝜑

Theoremnfdc 1565 If 𝑥 is not free in 𝜑, it is not free in DECID 𝜑. (Contributed by Jim Kingdon, 11-Mar-2018.)
𝑥𝜑       𝑥DECID 𝜑

Theoremmodal-5 1566 The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
(¬ ∀𝑥 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)

Theorem19.9d 1567 A deduction version of one direction of 19.9 1551. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
(𝜓 → Ⅎ𝑥𝜑)       (𝜓 → (∃𝑥𝜑𝜑))

Theorem19.9hd 1568 A deduction version of one direction of 19.9 1551. This is an older variation of this theorem; new proofs should use 19.9d 1567. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
(𝜓 → ∀𝑥𝜓)    &   (𝜓 → (𝜑 → ∀𝑥𝜑))       (𝜓 → (∃𝑥𝜑𝜑))

Theoremexcomim 1569 One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
(∃𝑥𝑦𝜑 → ∃𝑦𝑥𝜑)

Theoremexcom 1570 Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
(∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)

Theorem19.12 1571 Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.)
(∃𝑥𝑦𝜑 → ∀𝑦𝑥𝜑)

Theorem19.19 1572 Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
𝑥𝜑       (∀𝑥(𝜑𝜓) → (𝜑 ↔ ∃𝑥𝜓))

Theorem19.21-2 1573 Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)
𝑥𝜑    &   𝑦𝜑       (∀𝑥𝑦(𝜑𝜓) ↔ (𝜑 → ∀𝑥𝑦𝜓))

Theoremnf2 1574 An alternative definition of df-nf 1366, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)
(Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))

Theoremnf3 1575 An alternative definition of df-nf 1366. (Contributed by Mario Carneiro, 24-Sep-2016.)
(Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑𝜑))

Theoremnf4dc 1576 Variable 𝑥 is effectively not free in 𝜑 iff 𝜑 is always true or always false, given a decidability condition. The reverse direction, nf4r 1577, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.)
(DECID𝑥𝜑 → (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑)))

Theoremnf4r 1577 If 𝜑 is always true or always false, then variable 𝑥 is effectively not free in 𝜑. The converse holds given a decidability condition, as seen at nf4dc 1576. (Contributed by Jim Kingdon, 21-Jul-2018.)
((∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑) → Ⅎ𝑥𝜑)

Theorem19.36i 1578 Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
𝑥𝜓    &   𝑥(𝜑𝜓)       (∀𝑥𝜑𝜓)

Theorem19.36-1 1579 Closed form of 19.36i 1578. One direction of Theorem 19.36 of [Margaris] p. 90. The converse holds in classical logic, but does not hold (for all propositions) in intuitionistic logic. (Contributed by Jim Kingdon, 20-Jun-2018.)
𝑥𝜓       (∃𝑥(𝜑𝜓) → (∀𝑥𝜑𝜓))

Theorem19.37-1 1580 One direction of Theorem 19.37 of [Margaris] p. 90. The converse holds in classical logic but not, in general, here. (Contributed by Jim Kingdon, 21-Jun-2018.)
𝑥𝜑       (∃𝑥(𝜑𝜓) → (𝜑 → ∃𝑥𝜓))

Theorem19.37aiv 1581* Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
𝑥(𝜑𝜓)       (𝜑 → ∃𝑥𝜓)

Theorem19.38 1582 Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))

Theorem19.23t 1583 Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
(Ⅎ𝑥𝜓 → (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓)))

Theorem19.23 1584 Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)
𝑥𝜓       (∀𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))

Theorem19.32dc 1585 Theorem 19.32 of [Margaris] p. 90, where 𝜑 is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
𝑥𝜑       (DECID 𝜑 → (∀𝑥(𝜑𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)))

Theorem19.32r 1586 One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if 𝜑 is decidable, as seen at 19.32dc 1585. (Contributed by Jim Kingdon, 28-Jul-2018.)
𝑥𝜑       ((𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))

Theorem19.31r 1587 One direction of Theorem 19.31 of [Margaris] p. 90. The converse holds in classical logic, but not intuitionistic logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
𝑥𝜓       ((∀𝑥𝜑𝜓) → ∀𝑥(𝜑𝜓))

Theorem19.44 1588 Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
𝑥𝜓       (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))

Theorem19.45 1589 Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
𝑥𝜑       (∃𝑥(𝜑𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓))

Theorem19.34 1590 Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑𝜓))

Theorem19.41h 1591 Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1592 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)
(𝜓 → ∀𝑥𝜓)       (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))

Theorem19.41 1592 Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)
𝑥𝜓       (∃𝑥(𝜑𝜓) ↔ (∃𝑥𝜑𝜓))

Theorem19.42h 1593 Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1594 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.)
(𝜑 → ∀𝑥𝜑)       (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Theorem19.42 1594 Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
𝑥𝜑       (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Theoremexcom13 1595 Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)
(∃𝑥𝑦𝑧𝜑 ↔ ∃𝑧𝑦𝑥𝜑)

Theoremexrot3 1596 Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
(∃𝑥𝑦𝑧𝜑 ↔ ∃𝑦𝑧𝑥𝜑)

Theoremexrot4 1597 Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
(∃𝑥𝑦𝑧𝑤𝜑 ↔ ∃𝑧𝑤𝑥𝑦𝜑)

Theoremnexr 1598 Inference from 19.8a 1498. (Contributed by Jeff Hankins, 26-Jul-2009.)
¬ ∃𝑥𝜑        ¬ 𝜑

Theoremexan 1599 Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(∃𝑥𝜑𝜓)       𝑥(𝜑𝜓)

Theoremhbexd 1600 Deduction form of bound-variable hypothesis builder hbex 1543. (Contributed by NM, 2-Jan-2002.)
(𝜑 → ∀𝑦𝜑)    &   (𝜑 → (𝜓 → ∀𝑥𝜓))       (𝜑 → (∃𝑦𝜓 → ∀𝑥𝑦𝜓))

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-10511
 Copyright terms: Public domain < Previous  Next >