Theorem List for Intuitionistic Logic Explorer - 1801-1900 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | equs5 1801 |
Lemma used in proofs of substitution properties. (Contributed by NM,
5-Aug-1993.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | equs5or 1802 |
Lemma used in proofs of substitution properties. Like equs5 1801 but, in
intuitionistic logic, replacing negation and implication with
disjunction makes this a stronger result. (Contributed by Jim Kingdon,
2-Feb-2018.)
|
⊢ (∀𝑥 𝑥 = 𝑦 ∨ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | sb3 1803 |
One direction of a simplified definition of substitution when variables
are distinct. (Contributed by NM, 5-Aug-1993.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) |
|
Theorem | sb4 1804 |
One direction of a simplified definition of substitution when variables
are distinct. (Contributed by NM, 5-Aug-1993.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | sb4or 1805 |
One direction of a simplified definition of substitution when variables
are distinct. Similar to sb4 1804 but stronger in intuitionistic logic.
(Contributed by Jim Kingdon, 2-Feb-2018.)
|
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | sb4b 1806 |
Simplified definition of substitution when variables are distinct.
(Contributed by NM, 27-May-1997.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | sb4bor 1807 |
Simplified definition of substitution when variables are distinct,
expressed via disjunction. (Contributed by Jim Kingdon, 18-Mar-2018.)
|
⊢ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) |
|
Theorem | hbsb2 1808 |
Bound-variable hypothesis builder for substitution. (Contributed by NM,
5-Aug-1993.)
|
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) |
|
Theorem | nfsb2or 1809 |
Bound-variable hypothesis builder for substitution. Similar to hbsb2 1808
but in intuitionistic logic a disjunction is stronger than an implication.
(Contributed by Jim Kingdon, 2-Feb-2018.)
|
⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥[𝑦 / 𝑥]𝜑) |
|
Theorem | sbequilem 1810 |
Propositional logic lemma used in the sbequi 1811 proof. (Contributed by
Jim Kingdon, 1-Feb-2018.)
|
⊢ (𝜑 ∨ (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜏 ∨ (𝜓 → (𝜃 → 𝜂))) ⇒ ⊢ (𝜑 ∨ (𝜏 ∨ (𝜓 → (𝜒 → 𝜂)))) |
|
Theorem | sbequi 1811 |
An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
(Proof modified by Jim Kingdon, 1-Feb-2018.)
|
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) |
|
Theorem | sbequ 1812 |
An equality theorem for substitution. Used in proof of Theorem 9.7 in
[Megill] p. 449 (p. 16 of the preprint).
(Contributed by NM,
5-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
|
Theorem | drsb2 1813 |
Formula-building lemma for use with the Distinctor Reduction Theorem.
Part of Theorem 9.4 of [Megill] p. 448 (p.
16 of preprint). (Contributed
by NM, 27-Feb-2005.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
|
Theorem | spsbe 1814 |
A specialization theorem, mostly the same as Theorem 19.8 of [Margaris]
p. 89. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon,
29-Dec-2017.)
|
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑) |
|
Theorem | spsbim 1815 |
Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof
rewritten by Jim Kingdon, 21-Jan-2018.)
|
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
|
Theorem | spsbbi 1816 |
Specialization of biconditional. (Contributed by NM, 5-Aug-1993.) (Proof
rewritten by Jim Kingdon, 21-Jan-2018.)
|
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) |
|
Theorem | sbbidh 1817 |
Deduction substituting both sides of a biconditional. New proofs should
use sbbid 1818 instead. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.)
|
⊢ (𝜑 → ∀𝑥𝜑)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) |
|
Theorem | sbbid 1818 |
Deduction substituting both sides of a biconditional. (Contributed by
NM, 30-Jun-1993.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) |
|
Theorem | sbequ8 1819 |
Elimination of equality from antecedent after substitution. (Contributed
by NM, 5-Aug-1993.) (Proof revised by Jim Kingdon, 20-Jan-2018.)
|
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) |
|
Theorem | sbft 1820 |
Substitution has no effect on a non-free variable. (Contributed by NM,
30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened
by Wolf Lammen, 3-May-2018.)
|
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) |
|
Theorem | sbid2h 1821 |
An identity law for substitution. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) |
|
Theorem | sbid2 1822 |
An identity law for substitution. (Contributed by NM, 5-Aug-1993.)
(Revised by Mario Carneiro, 6-Oct-2016.)
|
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) |
|
Theorem | sbidm 1823 |
An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.)
(Proof rewritten by Jim Kingdon, 21-Jan-2018.)
|
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) |
|
Theorem | sb5rf 1824 |
Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Proof
shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑)) |
|
Theorem | sb6rf 1825 |
Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑)) |
|
Theorem | sb8h 1826 |
Substitution of variable in universal quantifier. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof
shortened by Jim Kingdon, 15-Jan-2018.)
|
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) |
|
Theorem | sb8eh 1827 |
Substitution of variable in existential quantifier. (Contributed by NM,
12-Aug-1993.) (Proof rewritten by Jim Kingdon, 15-Jan-2018.)
|
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) |
|
Theorem | sb8 1828 |
Substitution of variable in universal quantifier. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened
by Jim Kingdon, 15-Jan-2018.)
|
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) |
|
Theorem | sb8e 1829 |
Substitution of variable in existential quantifier. (Contributed by NM,
12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof
shortened by Jim Kingdon, 15-Jan-2018.)
|
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) |
|
1.4.4 Predicate calculus with distinct variables
(cont.)
|
|
Theorem | ax16i 1830* |
Inference with ax-16 1786 as its conclusion, that doesn't require ax-10 1483,
ax-11 1484, or ax-12 1489 for its proof. The hypotheses may be
eliminable
without one or more of these axioms in special cases. (Contributed by
NM, 20-May-2008.)
|
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) |
|
Theorem | ax16ALT 1831* |
Version of ax16 1785 that doesn't require ax-10 1483 or ax-12 1489 for its proof.
(Contributed by NM, 17-May-2008.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) |
|
Theorem | spv 1832* |
Specialization, using implicit substitition. (Contributed by NM,
30-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | spimev 1833* |
Distinct-variable version of spime 1719. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) |
|
Theorem | speiv 1834* |
Inference from existential specialization, using implicit substitition.
(Contributed by NM, 19-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 |
|
Theorem | equvin 1835* |
A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦)) |
|
Theorem | a16g 1836* |
A generalization of axiom ax-16 1786. (Contributed by NM, 5-Aug-1993.)
(Proof shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) |
|
Theorem | a16gb 1837* |
A generalization of axiom ax-16 1786. (Contributed by NM, 5-Aug-1993.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) |
|
Theorem | a16nf 1838* |
If there is only one element in the universe, then everything satisfies
Ⅎ. (Contributed by Mario Carneiro,
7-Oct-2016.)
|
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) |
|
Theorem | 2albidv 1839* |
Formula-building rule for 2 existential quantifiers (deduction form).
(Contributed by NM, 4-Mar-1997.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
|
Theorem | 2exbidv 1840* |
Formula-building rule for 2 existential quantifiers (deduction form).
(Contributed by NM, 1-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒)) |
|
Theorem | 3exbidv 1841* |
Formula-building rule for 3 existential quantifiers (deduction form).
(Contributed by NM, 1-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧𝜓 ↔ ∃𝑥∃𝑦∃𝑧𝜒)) |
|
Theorem | 4exbidv 1842* |
Formula-building rule for 4 existential quantifiers (deduction form).
(Contributed by NM, 3-Aug-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜓 ↔ ∃𝑥∃𝑦∃𝑧∃𝑤𝜒)) |
|
Theorem | 19.9v 1843* |
Special case of Theorem 19.9 of [Margaris] p.
89. (Contributed by NM,
28-May-1995.) (Revised by NM, 21-May-2007.)
|
⊢ (∃𝑥𝜑 ↔ 𝜑) |
|
Theorem | exlimdd 1844 |
Existential elimination rule of natural deduction. (Contributed by
Mario Carneiro, 9-Feb-2017.)
|
⊢ Ⅎ𝑥𝜑
& ⊢ Ⅎ𝑥𝜒
& ⊢ (𝜑 → ∃𝑥𝜓)
& ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | 19.21v 1845* |
Special case of Theorem 19.21 of [Margaris] p.
90. Notational
convention: We sometimes suffix with "v" the label of a
theorem
eliminating a hypothesis such as (𝜑 → ∀𝑥𝜑) in 19.21 1562 via
the use of distinct variable conditions combined with ax-17 1506.
Conversely, we sometimes suffix with "f" the label of a
theorem
introducing such a hypothesis to eliminate the need for the distinct
variable condition; e.g., euf 2002 derived from df-eu 2000. The "f" stands
for "not free in" which is less restrictive than "does
not occur in".
(Contributed by NM, 5-Aug-1993.)
|
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
|
Theorem | alrimiv 1846* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) |
|
Theorem | alrimivv 1847* |
Inference from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
31-Jul-1995.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥∀𝑦𝜓) |
|
Theorem | alrimdv 1848* |
Deduction from Theorem 19.21 of [Margaris] p.
90. (Contributed by NM,
10-Feb-1997.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) |
|
Theorem | nfdv 1849* |
Apply the definition of not-free in a context. (Contributed by Mario
Carneiro, 11-Aug-2016.)
|
⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) |
|
Theorem | 2ax17 1850* |
Quantification of two variables over a formula in which they do not
occur. (Contributed by Alan Sare, 12-Apr-2011.)
|
⊢ (𝜑 → ∀𝑥∀𝑦𝜑) |
|
Theorem | alimdv 1851* |
Deduction from Theorem 19.20 of [Margaris] p.
90. (Contributed by NM,
3-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
|
Theorem | eximdv 1852* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
27-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) |
|
Theorem | 2alimdv 1853* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
27-Apr-2004.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 → ∀𝑥∀𝑦𝜒)) |
|
Theorem | 2eximdv 1854* |
Deduction from Theorem 19.22 of [Margaris] p.
90. (Contributed by NM,
3-Aug-1995.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → ∃𝑥∃𝑦𝜒)) |
|
Theorem | 19.23v 1855* |
Special case of Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
28-Jun-1998.)
|
⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) |
|
Theorem | 19.23vv 1856* |
Theorem 19.23 of [Margaris] p. 90 extended to
two variables.
(Contributed by NM, 10-Aug-2004.)
|
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥∃𝑦𝜑 → 𝜓)) |
|
Theorem | sb56 1857* |
Two equivalent ways of expressing the proper substitution of 𝑦 for
𝑥 in 𝜑, when 𝑥 and 𝑦 are
distinct. Theorem 6.2 of
[Quine] p. 40. The proof does not involve
df-sb 1736. (Contributed by
NM, 14-Apr-2008.)
|
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
|
Theorem | sb6 1858* |
Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40.
Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM,
18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
|
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) |
|
Theorem | sb5 1859* |
Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
(Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
|
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) |
|
Theorem | sbnv 1860* |
Version of sbn 1923 where 𝑥 and 𝑦 are distinct.
(Contributed by
Jim Kingdon, 18-Dec-2017.)
|
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) |
|
Theorem | sbanv 1861* |
Version of sban 1926 where 𝑥 and 𝑦 are distinct.
(Contributed by
Jim Kingdon, 24-Dec-2017.)
|
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) |
|
Theorem | sborv 1862* |
Version of sbor 1925 where 𝑥 and 𝑦 are distinct.
(Contributed by
Jim Kingdon, 3-Feb-2018.)
|
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) |
|
Theorem | sbi1v 1863* |
Forward direction of sbimv 1865. (Contributed by Jim Kingdon,
25-Dec-2017.)
|
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
|
Theorem | sbi2v 1864* |
Reverse direction of sbimv 1865. (Contributed by Jim Kingdon,
18-Jan-2018.)
|
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) |
|
Theorem | sbimv 1865* |
Intuitionistic proof of sbim 1924 where 𝑥 and 𝑦 are distinct.
(Contributed by Jim Kingdon, 18-Jan-2018.)
|
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) |
|
Theorem | sblimv 1866* |
Version of sblim 1928 where 𝑥 and 𝑦 are distinct.
(Contributed by
Jim Kingdon, 19-Jan-2018.)
|
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)) |
|
Theorem | pm11.53 1867* |
Theorem *11.53 in [WhiteheadRussell]
p. 164. (Contributed by Andrew
Salmon, 24-May-2011.)
|
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓)) |
|
Theorem | exlimivv 1868* |
Inference from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
1-Aug-1995.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥∃𝑦𝜑 → 𝜓) |
|
Theorem | exlimdvv 1869* |
Deduction from Theorem 19.23 of [Margaris] p.
90. (Contributed by NM,
31-Jul-1995.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 → 𝜒)) |
|
Theorem | exlimddv 1870* |
Existential elimination rule of natural deduction. (Contributed by
Mario Carneiro, 15-Jun-2016.)
|
⊢ (𝜑 → ∃𝑥𝜓)
& ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | 19.27v 1871* |
Theorem 19.27 of [Margaris] p. 90.
(Contributed by NM, 3-Jun-2004.)
|
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) |
|
Theorem | 19.28v 1872* |
Theorem 19.28 of [Margaris] p. 90.
(Contributed by NM, 25-Mar-2004.)
|
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) |
|
Theorem | 19.36aiv 1873* |
Inference from Theorem 19.36 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | 19.41v 1874* |
Special case of Theorem 19.41 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) |
|
Theorem | 19.41vv 1875* |
Theorem 19.41 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 30-Apr-1995.)
|
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) |
|
Theorem | 19.41vvv 1876* |
Theorem 19.41 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 30-Apr-1995.)
|
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) |
|
Theorem | 19.41vvvv 1877* |
Theorem 19.41 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
FL, 14-Jul-2007.)
|
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (∃𝑤∃𝑥∃𝑦∃𝑧𝜑 ∧ 𝜓)) |
|
Theorem | 19.42v 1878* |
Special case of Theorem 19.42 of [Margaris] p.
90. (Contributed by NM,
5-Aug-1993.)
|
⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) |
|
Theorem | spvv 1879* |
Version of spv 1832 with a disjoint variable condition.
(Contributed by
BJ, 31-May-2019.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) |
|
Theorem | chvarvv 1880* |
Version of chvarv 1907 with a disjoint variable condition.
(Contributed by
BJ, 31-May-2019.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | exdistr 1881* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.)
|
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) |
|
Theorem | exdistrv 1882* |
Distribute a pair of existential quantifiers (over disjoint variables)
over a conjunction. Combination of 19.41v 1874 and 19.42v 1878. For a
version with fewer disjoint variable conditions but requiring more
axioms, see eeanv 1902. (Contributed by BJ, 30-Sep-2022.)
|
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
|
Theorem | 19.42vv 1883* |
Theorem 19.42 of [Margaris] p. 90 with 2
quantifiers. (Contributed by
NM, 16-Mar-1995.)
|
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
|
Theorem | 19.42vvv 1884* |
Theorem 19.42 of [Margaris] p. 90 with 3
quantifiers. (Contributed by
NM, 21-Sep-2011.)
|
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓)) |
|
Theorem | 19.42vvvv 1885* |
Theorem 19.42 of [Margaris] p. 90 with 4
quantifiers. (Contributed by
Jim Kingdon, 23-Nov-2019.)
|
⊢ (∃𝑤∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑤∃𝑥∃𝑦∃𝑧𝜓)) |
|
Theorem | exdistr2 1886* |
Distribution of existential quantifiers. (Contributed by NM,
17-Mar-1995.)
|
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓)) |
|
Theorem | 3exdistr 1887* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒))) |
|
Theorem | 4exdistr 1888* |
Distribution of existential quantifiers. (Contributed by NM,
9-Mar-1995.)
|
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃)))) |
|
Theorem | cbvalv 1889* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
|
Theorem | cbvexv 1890* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
|
Theorem | cbval2 1891* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro,
6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) |
|
Theorem | cbvex2 1892* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro,
6-Oct-2016.)
|
⊢ Ⅎ𝑧𝜑
& ⊢ Ⅎ𝑤𝜑
& ⊢ Ⅎ𝑥𝜓
& ⊢ Ⅎ𝑦𝜓
& ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) |
|
Theorem | cbval2v 1893* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 4-Feb-2005.)
|
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) |
|
Theorem | cbvex2v 1894* |
Rule used to change bound variables, using implicit substitution.
(Contributed by NM, 26-Jul-1995.)
|
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) |
|
Theorem | cbvald 1895* |
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 1990. (Contributed by NM,
2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf
Lammen, 13-May-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑦𝜓)
& ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
|
Theorem | cbvexdh 1896* |
Deduction used to change bound variables, using implicit substitition,
particularly useful in conjunction with dvelim 1990. (Contributed by NM,
2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
|
⊢ (𝜑 → ∀𝑦𝜑)
& ⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) |
|
Theorem | cbvexd 1897* |
Deduction used to change bound variables, using implicit substitution,
particularly useful in conjunction with dvelim 1990. (Contributed by NM,
2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof rewritten
by Jim Kingdon, 10-Jun-2018.)
|
⊢ Ⅎ𝑦𝜑
& ⊢ (𝜑 → Ⅎ𝑦𝜓)
& ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) |
|
Theorem | cbvaldva 1898* |
Rule used to change the bound variable in a universal quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) |
|
Theorem | cbvexdva 1899* |
Rule used to change the bound variable in an existential quantifier with
implicit substitution. Deduction form. (Contributed by David Moews,
1-May-2017.)
|
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) |
|
Theorem | cbvex4v 1900* |
Rule used to change bound variables, using implicit substitition.
(Contributed by NM, 26-Jul-1995.)
|
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) |