![]() |
Metamath
Proof Explorer Theorem List (p. 20 of 437) | < 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: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfnt 1901 | If a variable is non-free in a proposition, then it is non-free in its negation. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) df-nf 1828 changed. (Revised by Wolf Lammen, 4-Oct-2021.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfn 1902 | Inference associated with nfnt 1901. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1828 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥 ¬ 𝜑 | ||
Theorem | nfnd 1903 | Deduction associated with nfnt 1901. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | ||
Theorem | exanali 1904 | A transformation of quantifiers and logical connectives. (Contributed by NM, 25-Mar-1996.) (Proof shortened by Wolf Lammen, 4-Sep-2014.) |
⊢ (∃𝑥(𝜑 ∧ ¬ 𝜓) ↔ ¬ ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | exancom 1905 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | exan 1906 | 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, 6-Nov-2022.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | exanOLD 1907 | Obsolete proof of exan 1906 as of 6-Nov-2022. (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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥𝜑 ∧ 𝜓) ⇒ ⊢ ∃𝑥(𝜑 ∧ 𝜓) | ||
Theorem | alrimdh 1908 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2192 and 19.21h 2261. (Contributed by NM, 10-Feb-1997.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdh 1909 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | nexdh 1910 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albidh 1911 | Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidh 1912 | Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | exsimpl 1913 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜑) | ||
Theorem | exsimpr 1914 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → ∃𝑥𝜓) | ||
Theorem | 19.40 1915 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 26-May-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.26 1916 | 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 1917 | Theorem 19.26 1916 with two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥∀𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.26-3an 1918 | Theorem 19.26 1916 with triple conjunction. (Contributed by NM, 13-Sep-2011.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | 19.26-3anOLD 1919 | Obsolete version of 19.26-3an 1918 as of 10-Jul-2022. (Contributed by NM, 13-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | 19.29 1920 | Theorem 19.29 of [Margaris] p. 90. See also 19.29r 1921. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((∀𝑥𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r 1921 | Variation of 19.29 1920. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2020.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29r2 1922 | Variation of 19.29r 1921 with double quantification. (Contributed by NM, 3-Feb-2005.) |
⊢ ((∃𝑥∃𝑦𝜑 ∧ ∀𝑥∀𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.29x 1923 | Variation of 19.29 1920 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
⊢ ((∃𝑥∀𝑦𝜑 ∧ ∀𝑥∃𝑦𝜓) → ∃𝑥∃𝑦(𝜑 ∧ 𝜓)) | ||
Theorem | 19.35 1924 | 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 1925 | Inference associated with 19.35 1924. (Contributed by NM, 21-Jun-1993.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.35ri 1926 | Inference associated with 19.35 1924. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑥𝜑 → ∃𝑥𝜓) ⇒ ⊢ ∃𝑥(𝜑 → 𝜓) | ||
Theorem | 19.25 1927 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ (∀𝑦∃𝑥(𝜑 → 𝜓) → (∃𝑦∀𝑥𝜑 → ∃𝑦∃𝑥𝜓)) | ||
Theorem | 19.30 1928 | Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43 1929 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 27-Jun-2014.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.43OLD 1930 | Obsolete proof of 19.43 1929. Do not delete as it is referenced on the mmrecent.html page and in conventions-labels 27833. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | 19.33 1931 | Theorem 19.33 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | 19.33b 1932 | The antecedent provides a condition implying the converse of 19.33 1931. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.) |
⊢ (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓))) | ||
Theorem | 19.40-2 1933 | Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with two quantifiers. (Contributed by Andrew Salmon, 24-May-2011.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → (∃𝑥∃𝑦𝜑 ∧ ∃𝑥∃𝑦𝜓)) | ||
Theorem | 19.40b 1934 | The antecedent provides a condition implying the converse of 19.40 1915. This is to 19.40 1915 what 19.33b 1932 is to 19.33 1931. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.) |
⊢ ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | albiim 1935 | Split a biconditional and distribute quantifier. (Contributed by NM, 18-Aug-1993.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) ↔ (∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜑))) | ||
Theorem | 2albiim 1936 | Split a biconditional and distribute two quantifiers. (Contributed by NM, 3-Feb-2005.) |
⊢ (∀𝑥∀𝑦(𝜑 ↔ 𝜓) ↔ (∀𝑥∀𝑦(𝜑 → 𝜓) ∧ ∀𝑥∀𝑦(𝜓 → 𝜑))) | ||
Theorem | exintrbi 1937 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | exintr 1938 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) (Proof shortened by BJ, 16-Sep-2022.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓))) | ||
Theorem | alsyl 1939 | Universally quantified and uncurried (imported) form of syllogism. Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
⊢ ((∀𝑥(𝜑 → 𝜓) ∧ ∀𝑥(𝜓 → 𝜒)) → ∀𝑥(𝜑 → 𝜒)) | ||
Theorem | nfimd 1940 | If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 → 𝜒). Deduction form of nfim 1943. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1828 changed. (Revised by Wolf Lammen, 18-Sep-2021.) Eliminate curried form of nfimt 1941. (Revised by Wolf Lammen, 10-Jul-2022.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | nfimt 1941 | Closed form of nfim 1943 and nfimd 1940. (Contributed by BJ, 20-Oct-2021.) Eliminate curried form, former name nfimt2. (Revised by Wolf Lammen, 6-Jul-2022.) |
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓)) | ||
Theorem | nfimdOLDOLD 1942 | Obsolete version of nfimd 1940 as of 6-Jul-2022. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) df-nf 1828 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | nfim 1943 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1941. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1828 changed. (Revised by Wolf Lammen, 17-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 → 𝜓) | ||
Theorem | nfand 1944 | If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | nf3and 1945 | Deduction form of bound-variable hypothesis builder nf3an 1948. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝜃) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | nfan 1946 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∧ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 9-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | ||
Theorem | nfnan 1947 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ⊼ 𝜓). (Contributed by Scott Fenton, 2-Jan-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ⊼ 𝜓) | ||
Theorem | nf3an 1948 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, then it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) | ||
Theorem | nfbid 1949 | If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ↔ 𝜒). (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | nfbi 1950 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) | ||
Theorem | nfor 1951 | If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∨ 𝜓). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) | ||
Theorem | nf3or 1952 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, then it is not free in (𝜑 ∨ 𝜓 ∨ 𝜒). (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Axiom | ax-5 1953* |
Axiom of Distinctness. This axiom quantifies a variable over a formula
in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of [Monk2] p. 113.
(See comments in ax5ALT 35061 about the logical redundancy of ax-5 1953 in the presence of our obsolete axioms.) This axiom essentially says that if 𝑥 does not occur in 𝜑, i.e. 𝜑 does not depend on 𝑥 in any way, then we can add the quantifier ∀𝑥 to 𝜑 with no further assumptions. By sp 2167, we can also remove the quantifier (unconditionally). (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) | ||
Theorem | ax5d 1954* | Version of ax-5 1953 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders. (Contributed by NM, 1-Mar-2013.) |
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | ax5e 1955* | A rephrasing of ax-5 1953 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.) |
⊢ (∃𝑥𝜑 → 𝜑) | ||
Theorem | ax5ea 1956* | If a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable. (Contributed by BJ, 28-Dec-2020.) |
⊢ (∃𝑥𝜑 → ∀𝑥𝜑) | ||
Theorem | nfv 1957* | If 𝑥 is not present in 𝜑, then 𝑥 is not free in 𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) Definition change. (Revised by Wolf Lammen, 12-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfvd 1958* | nfv 1957 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1940. (Contributed by Mario Carneiro, 6-Oct-2016.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | alimdv 1959* | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1854. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximdv 1960* | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1877. (Contributed by NM, 27-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | 2alimdv 1961* | Deduction form of Theorem 19.20 of [Margaris] p. 90 with two quantifiers, see alim 1854. (Contributed by NM, 27-Apr-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2eximdv 1962* | Deduction form of Theorem 19.22 of [Margaris] p. 90 with two quantifiers, see exim 1877. (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) | ||
Theorem | albidv 1963* | Formula-building rule for universal quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbidv 1964* | Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | nfbidv 1965* | An equality theorem for nonfreeness. See nfbidf 2210 for a version without disjoint variable condition but requiring more axioms. (Contributed by Mario Carneiro, 4-Oct-2016.) Remove dependency on ax-6 2021, ax-7 2055, ax-12 2163 by adapting proof of nfbidf 2210. (Revised by BJ, 25-Sep-2022.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
Theorem | 2albidv 1966* | Formula-building rule for two universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) | ||
Theorem | 2exbidv 1967* | Formula-building rule for two existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) | ||
Theorem | 3exbidv 1968* | Formula-building rule for three existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧𝜓 ↔ ∃𝑥∃𝑦∃𝑧𝜒)) | ||
Theorem | 4exbidv 1969* | Formula-building rule for four existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) | ||
Theorem | alrimiv 1970* | Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2192 and 19.21v 1982. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | alrimivv 1971* | Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2192 and 19.21v 1982. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) | ||
Theorem | alrimdv 1972* | Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2192 and 19.21v 1982. (Contributed by NM, 10-Feb-1997.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | exlimiv 1973* |
Inference form of Theorem 19.23 of [Margaris]
p. 90, see 19.23 2197.
See exlimi 2203 for a more general version requiring more axioms. This inference, along with its many variants such as rexlimdv 3212, 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.appstate.edu/~hirstjl/primer/hirst.pdf. In informal proofs, the statement "Let 𝐶 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 𝜑(𝐶) as a hypothesis for the proof where 𝐶 is a new (fictitious) 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 1973 to arrive at (∃𝑥𝜑 → 𝜓). Finally, we separately prove ∃𝑥𝜑 and detach it with modus ponens ax-mp 5 to arrive at the final theorem 𝜓, see exlimiiv 1974. (Contributed by NM, 21-Jun-1993.) Remove dependencies on ax-6 2021 and ax-8 2109. (Revised by Wolf Lammen, 4-Dec-2017.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exlimiiv 1974* | Inference (Rule C) associated with exlimiv 1973. (Contributed by BJ, 19-Dec-2020.) |
⊢ (𝜑 → 𝜓) & ⊢ ∃𝑥𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | exlimivv 1975* | Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2197. (Contributed by NM, 1-Aug-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) | ||
Theorem | exlimdv 1976* | Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2197. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 2021, ax-7 2055. (Revised by Wolf Lammen, 4-Dec-2017.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | exlimdvv 1977* | Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2197. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) | ||
Theorem | exlimddv 1978* | Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1973). (Contributed by Mario Carneiro, 15-Jun-2016.) |
⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nexdv 1979* | Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | 2ax5 1980* | Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.) |
⊢ (𝜑 → ∀𝑥∀𝑦𝜑) | ||
Theorem | stdpc5v 1981* | Version of stdpc5 2193 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) Revised to shorten 19.21v 1982. (Revised by Wolf Lammen, 12-Jul-2020.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.21v 1982* |
Version of 19.21 2192 with a disjoint variable condition, requiring
fewer
axioms.
Notational convention: We sometimes suffix with "v" the label of a theorem using a distinct variable ("dv") condition instead of a non-freeness hypothesis such as Ⅎ𝑥𝜑. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a non-freeness hypothesis ("f" stands for "not free in", see df-nf 1828) instead of a disjoint variable condition. For instance, 19.21v 1982 versus 19.21 2192 and vtoclf 3459 versus vtocl 3460. Note that "not free in" is less restrictive than "does not occur in". Note that the version with a disjoint variable condition is easily proved from the version with the corresponding non-freeness hypothesis, by using nfv 1957. However, the dv version can often be proved from fewer axioms. (Contributed by NM, 21-Jun-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 12-Jul-2020.) |
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.32v 1983* | Version of 19.32 2219 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | 19.31v 1984* | Version of 19.31 2220 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) |
⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.23v 1985* | Version of 19.23 2197 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.) Remove dependency on ax-6 2021. (Revised by Rohan Ridenour, 15-Apr-2022.) |
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | 19.23vv 1986* | Theorem 19.23v 1985 extended to two variables. (Contributed by NM, 10-Aug-2004.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓)) | ||
Theorem | pm11.53v 1987* | Version of pm11.53 2315 with a disjoint variable condition, requiring fewer axioms. (Contributed by BJ, 7-Mar-2020.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) | ||
Theorem | 19.36imv 1988* | One direction of 19.36v 2036 that can be proven without ax-6 2021. (Contributed by Rohan Ridenour, 16-Apr-2022.) |
⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | 19.36iv 1989* | Inference associated with 19.36v 2036. Version of 19.36i 2217 with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) Remove dependency on ax-6 2021. (Revised by Rohan Ridenour, 15-Apr-2022.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.37imv 1990* | One direction of 19.37v 2040 that can be proven without ax-6 2021. (Contributed by Rohan Ridenour, 16-Apr-2022.) |
⊢ (∃𝑥(𝜑 → 𝜓) → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.37iv 1991* | Inference associated with 19.37v 2040. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-6 2021. (Revised by Rohan Ridenour, 15-Apr-2022.) |
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.41v 1992* | Version of 19.41 2221 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-6 2021. (Revised by Rohan Ridenour, 15-Apr-2022.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vv 1993* | Version of 19.41 2221 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvv 1994* | Version of 19.41 2221 with three quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.41vvvv 1995* | Version of 19.41 2221 with four quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by FL, 14-Jul-2007.) |
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) | ||
Theorem | 19.42v 1996* | Version of 19.42 2223 with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | exdistr 1997* | Distribution of existential quantifiers. See also exdistrv 1998. (Contributed by NM, 9-Mar-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | exdistrv 1998* | Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1992 and 19.42v 1996. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2318. (Contributed by BJ, 30-Sep-2022.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) | ||
Theorem | 4exdistrv 1999* | Distribute two pairs of existential quantifiers (over disjoint variables) over a conjunction. For a version with fewer disjoint variable conditions but requiring more axioms, see ee4anv 2320. (Contributed by BJ, 5-Jan-2023.) |
⊢ (∃𝑥∃𝑧∃𝑦∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓)) | ||
Theorem | 19.42vv 2000* | Version of 19.42 2223 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |