Home | Metamath
Proof Explorer Theorem List (p. 18 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-nf 1701 |
Define the not-free predicate for wffs. This is read "𝑥 is not
free
in 𝜑". Not-free means that the
value of 𝑥 cannot affect the
value of 𝜑, e.g., any occurrence of 𝑥 in
𝜑 is
effectively
bound by a "for all" or something that expands to one (such as
"there
exists"). In particular, substitution for a variable not free in a
wff
does not affect its value (sbf 2368). An example of where this is used is
stdpc5 2063. See nf5 2102 for an alternate definition which
involves nested
quantifiers on the same variable.
Not-free is a commonly used constraint, so it is useful to have a notation for it. Surprisingly, there is no common formal notation for it, so here we devise one. Our definition lets us work with the not-free notion within the logic itself rather than as a metalogical side condition. To be precise, our definition really means "effectively not free," because it is slightly less restrictive than the usual textbook definition for not-free (which only considers syntactic freedom). For example, 𝑥 is effectively not free in the bare expression 𝑥 = 𝑥 (see nfequid 1927), even though 𝑥 would be considered free in the usual textbook definition, because the value of 𝑥 in the expression 𝑥 = 𝑥 cannot affect the truth of the expression (and thus substitution will not change the result). This definition of not-free tightly ties to the quantifier ∀𝑥. At this state (no axioms restricting quantifiers yet) 'non-free' appears quite arbitrary. Its intended semantics expresses single-valuedness (constness) across a parameter, but is only evolved as much as later axioms assign properties to quantifiers. It seems the definition here is best suited in situations, where axioms are only partially in effect. In particular, this definition more easily carries over to other logic models with weaker axiomization. This predicate only applies to wffs. See df-nfc 2740 for a not-free predicate for class variables. (Contributed by Mario Carneiro, 24-Sep-2016.) Converted to definition. (Revised by BJ, 6-May-2019.) |
⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑)) | ||
Theorem | nf2 1702 | Alternate definition of non-freeness. (Contributed by BJ, 16-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ¬ ∃𝑥𝜑)) | ||
Theorem | nf3 1703 | Alternate definition of non-freeness. (Contributed by BJ, 16-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑)) | ||
Theorem | nf4 1704 | Alternate definition of non-freeness. This definition uses only primitive symbols. (Contributed by BJ, 16-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | nfi 1705 | Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Wolf Lammen, 15-Sep-2021.) |
⊢ (∃𝑥𝜑 → ∀𝑥𝜑) ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfri 1706 | Consequence of the definition of not-free. (Contributed by Wolf Lammen, 16-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | nfd 1707 | Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Wolf Lammen, 16-Sep-2021.) |
⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | nfrd 1708 | Consequence of the definition of not-free in a context. (Contributed by Wolf Lammen, 15-Oct-2021.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓)) | ||
Theorem | nftht0 1709 | Closed form of nfth 1718. (Contributed by Wolf Lammen, 19-Aug-2018.) (Proof shortened by BJ, 16-Sep-2021.) |
⊢ (∀𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | nfntht 1710 | Closed form of nfnth 1719. (Contributed by BJ, 16-Sep-2021.) |
⊢ (¬ ∃𝑥𝜑 → Ⅎ𝑥𝜑) | ||
Theorem | nfntht2 1711 | Closed form of nfnth 1719. (Contributed by BJ, 16-Sep-2021.) |
⊢ (∀𝑥 ¬ 𝜑 → Ⅎ𝑥𝜑) | ||
Definition | df-nfOLD 1712 | Obsolete definition replaced by nf5 2102 as of 3-Oct-2021. This definition is less suitable than df-nf 1701 when ax-10 2006 and ax-12 2034 are not in effect. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | ||
Axiom | ax-gen 1713 | Rule of Generalization. The postulated inference rule of predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved 𝑥 = 𝑥, we can conclude ∀𝑥𝑥 = 𝑥 or even ∀𝑦𝑥 = 𝑥. Theorem allt 31570 shows the special case ∀𝑥⊤. Theorem spi 2042 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (Contributed by NM, 3-Jan-1993.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥𝜑 | ||
Theorem | gen2 1714 | Generalization applied twice. (Contributed by NM, 30-Apr-1998.) |
⊢ 𝜑 ⇒ ⊢ ∀𝑥∀𝑦𝜑 | ||
Theorem | mpg 1715 | Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.) |
⊢ (∀𝑥𝜑 → 𝜓) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | mpgbi 1716 | Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
⊢ (∀𝑥𝜑 ↔ 𝜓) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | mpgbir 1717 | Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.) |
⊢ (𝜑 ↔ ∀𝑥𝜓) & ⊢ 𝜓 ⇒ ⊢ 𝜑 | ||
Theorem | nfth 1718 | No variable is (effectively) free in a theorem. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1701 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfnth 1719 | No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016.) df-nf 1701 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | hbth 1720 |
No variable is (effectively) free in a theorem.
This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form ⊢ (𝜑 → ∀𝑥𝜑) from smaller formulas of this form. These are useful for constructing hypotheses that state "𝑥 is (effectively) not free in 𝜑." (Contributed by NM, 11-May-1993.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | nftru 1721 | The true constant has no free variables. (This can also be proven in one step with nfv 1830, but this proof does not use ax-5 1827.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑥⊤ | ||
Theorem | nex 1722 | Generalization rule for negated wff. (Contributed by NM, 18-May-1994.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ ∃𝑥𝜑 | ||
Theorem | nffal 1723 | The false constant has no free variables (see nftru 1721). (Contributed by BJ, 6-May-2019.) |
⊢ Ⅎ𝑥⊥ | ||
Theorem | sptruw 1724 | Version of sp 2041 when 𝜑 is true. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) |
⊢ 𝜑 ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | nfiOLD 1725 | Obsolete proof of nf5i 2011 as of 5-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfthOLD 1726 | Obsolete proof of nfth 1718 as of 5-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfnthOLD 1727 | Obsolete proof of nfnth 1719 as of 6-Oct-2021. (Contributed by Mario Carneiro, 6-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ 𝜑 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Axiom | ax-4 1728 | Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105 and Theorem 19.20 of [Margaris] p. 90. It is restated as alim 1729 for labeling consistency. It should be used only by alim 1729. (Contributed by NM, 21-May-2008.) Use alim 1729 instead. (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | alim 1729 | Restatement of Axiom ax-4 1728, for labeling consistency. It should be the only theorem using ax-4 1728. (Contributed by NM, 10-Jan-1993.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | alimi 1730 | Inference quantifying both antecedent and consequent. (Contributed by NM, 5-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | 2alimi 1731 | Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦𝜓) | ||
Theorem | al2im 1732 | Closed form of al2imi 1733. Version of alim 1729 for a nested implication. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ (∀𝑥(𝜑 → (𝜓 → 𝜒)) → (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒))) | ||
Theorem | al2imi 1733 | Inference quantifying antecedent, nested antecedent, and consequent. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | alanimi 1734 | Variant of al2imi 1733 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥𝜒) | ||
Theorem | alimdh 1735 | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1729. (Contributed by NM, 4-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | albi 1736 | Theorem 19.15 of [Margaris] p. 90. (Contributed by NM, 24-Jan-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | albii 1737 | Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) | ||
Theorem | 2albii 1738 | Inference adding two universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) | ||
Theorem | sylgt 1739 | Closed form of sylg 1740. (Contributed by BJ, 2-May-2019.) |
⊢ (∀𝑥(𝜓 → 𝜒) → ((𝜑 → ∀𝑥𝜓) → (𝜑 → ∀𝑥𝜒))) | ||
Theorem | sylg 1740 | A syllogism combined with generalization. Inference associated with sylgt 1739. General form of alrimih 1741. (Contributed by BJ, 4-Oct-2019.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
Theorem | alrimih 1741 | Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2062 and 19.21h 2107. Instance of sylg 1740. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | hbxfrbi 1742 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. See hbxfreq 2717 for equality version. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | alex 1743 | Theorem 19.6 of [Margaris] p. 89. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑) | ||
Theorem | exnal 1744 | Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑) | ||
Theorem | 2nalexn 1745 | Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∀𝑥∀𝑦𝜑 ↔ ∃𝑥∃𝑦 ¬ 𝜑) | ||
Theorem | 2exnaln 1746 | Theorem *11.22 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | 2nexaln 1747 | Theorem *11.25 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | alimex 1748 | A utility theorem. An interesting case is when the same formula is substituted for both 𝜑 and 𝜓, since then both implications express a type of non-freeness. See also eximal 1698. (Contributed by BJ, 12-May-2019.) |
⊢ ((𝜑 → ∀𝑥𝜓) ↔ (∃𝑥 ¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | aleximi 1749 | A variant of al2imi 1733: instead of applying ∀𝑥 quantifiers to the final implication, replace them with ∃𝑥. A shorter proof is possible using nfa1 2015, sps 2043 and eximd 2072, but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | alexbii 1750 | Biconditional form of aleximi 1749. (Contributed by BJ, 16-Nov-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exim 1751 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | eximi 1752 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 2eximi 1753 | Inference adding two existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑥∃𝑦𝜓) | ||
Theorem | eximii 1754 | Inference associated with eximi 1752. (Contributed by BJ, 3-Feb-2018.) |
⊢ ∃𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ∃𝑥𝜓 | ||
Theorem | ala1 1755 | Add an antecedent in a universally quantified formula. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∀𝑥𝜑 → ∀𝑥(𝜓 → 𝜑)) | ||
Theorem | exa1 1756 | Add an antecedent in an existentially quantified formula. (Contributed by BJ, 6-Oct-2018.) |
⊢ (∃𝑥𝜑 → ∃𝑥(𝜓 → 𝜑)) | ||
Theorem | 19.38 1757 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) Allow a shortening of 19.21t 2061. (Revised by Wolf Lammen, 2-Jan-2018.) |
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | imnang 1758 | Quantified implication in terms of quantified negation of conjunction. (Contributed by BJ, 16-Jul-2021.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ∀𝑥 ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | alinexa 1759 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
⊢ (∀𝑥(𝜑 → ¬ 𝜓) ↔ ¬ ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | alexn 1760 | A relationship between two quantifiers and negation. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥∃𝑦 ¬ 𝜑 ↔ ¬ ∃𝑥∀𝑦𝜑) | ||
Theorem | 2exnexn 1761 | Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (Proof shortened by Wolf Lammen, 25-Sep-2014.) |
⊢ (∃𝑥∀𝑦𝜑 ↔ ¬ ∀𝑥∃𝑦 ¬ 𝜑) | ||
Theorem | exbi 1762 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | exbiOLD 1763 | Obsolete proof of exbi 1762 as of 16-Nov-2020. (Contributed by NM, 12-Mar-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | exbii 1764 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓) | ||
Theorem | 2exbii 1765 | Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜓) | ||
Theorem | 3exbii 1766 | Inference adding three existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧𝜑 ↔ ∃𝑥∃𝑦∃𝑧𝜓) | ||
Theorem | nfnt 1767 | 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.) df-nf 1701 changed. (Revised by Wolf Lammen, 4-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfn 1768 | Inference associated with nfnt 1767. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1701 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥 ¬ 𝜑 | ||
Theorem | nfnd 1769 | Deduction associated with nfnt 1767. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | ||
Theorem | nfbii 1770 | Equality theorem for not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1701 changed. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) | ||
Theorem | nfxfr 1771 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfxfrd 1772 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜒 → Ⅎ𝑥𝜑) | ||
Theorem | exanali 1773 | A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.) |
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | exancom 1774 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | exan 1775 | Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof shortened by Wolf Lammen, 8-Oct-2021.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | exanOLD 1776 | Obsolete proof of exan 1775 as of 8-Oct-2021. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) Reduce axiom dependencies. (Revised by BJ, 7-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | alrimdh 1777 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2062 and 19.21h 2107. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdh 1778 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | nexdh 1779 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albidh 1780 | Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidh 1781 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exbidhOLD 1782 | Obsolete proof of exbidh 1781 as of 16-Nov-2020. (Contributed by NM, 26-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exsimpl 1783 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) | ||
Theorem | exsimpr 1784 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓) | ||
Theorem | 19.40 1785 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.26 1786 | Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.26-2 1787 | Theorem 19.26 1786 with two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.26-3an 1788 | Theorem 19.26 1786 with triple conjunction. (Contributed by NM, 13-Sep-2011.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | 19.29 1789 | Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1790. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r 1790 | Variation of 19.29 1789. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29rOLD 1791 | Obsolete proof of 19.29r 1790 as 12-Nov-2020. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r2 1792 | Variation of 19.29r 1790 with double quantification. (Contributed by NM, 3-Feb-2005.) |
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29x 1793 | Variation of 19.29 1789 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.35 1794 | Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.35i 1795 | Inference associated with 19.35 1794. (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.35ri 1796 | Inference associated with 19.35 1794. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 → ∃𝑥𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | 19.25 1797 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓)) | ||
Theorem | 19.30 1798 | Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43 1799 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43OLD 1800 | Obsolete proof of 19.43 1799. Do not delete as it is referenced on the mmrecent.html page and in conventions-label 26651. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |