![]() |
Metamath
Proof Explorer Theorem List (p. 26 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbie 2501 | Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2308 and sbievw 2095. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbied 2502 | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2501) Usage of this theorem is discouraged because it depends on ax-13 2371. See sbiedw 2309, sbiedvw 2096 for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbiedv 2503* | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2501). Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker sbiedvw 2096 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | 2sbiev 2504* | Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See 2sbievw 2097 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbcom3 2505 | Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2098. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2154. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | sbco 2506 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. See sbcov 2248 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbid2 2507 | An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out sbid2vw 2250 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbid2v 2508* | An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2371. See sbid2vw 2250 for a version with an extra disjoint variable condition requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbidm 2509 | An idempotent law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2 2510 | A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2326 and sbco2vv 2100. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2d 2511 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbco3 2512 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) | ||
Theorem | sbcom 2513 | A commutativity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Check out sbcom3vv 2098 for a version requiring fewer axioms. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑) | ||
Theorem | sbtrt 2514 | Partially closed form of sbtr 2515. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑) | ||
Theorem | sbtr 2515 | A partial converse to sbt 2069. If the substitution of a variable for a nonfree one in a wff gives a theorem, then the original wff is a theorem. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by BJ, 15-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ [𝑦 / 𝑥]𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | sb8 2516 | Substitution of variable in universal quantifier. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring disjoint variables, but fewer axioms, see sb8f 2349. (Contributed by NM, 16-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8e 2517 | Substitution of variable in existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring disjoint variables, but fewer axioms, see sb8ef 2351. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb9 2518 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2519. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb9i 2519 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sbhb 2520* | Two ways of expressing "𝑥 is (effectively) not free in 𝜑". Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 29-May-2009.) (New usage is discouraged.) |
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsbd 2521* | Deduction version of nfsb 2522. (Contributed by NM, 15-Feb-2013.) Usage of this theorem is discouraged because it depends on ax-13 2371. Use nfsbv 2323 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓) | ||
Theorem | nfsb 2522* | If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2323 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2371. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on ax-13 2371. Use nfsbv 2323 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsb 2523* | If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by NM, 12-Aug-1993.) Usage of this theorem is discouraged because it depends on ax-13 2371. Use hbsbw 2169 instead. (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sb7f 2524* | This version of dfsb7 2275 does not require that 𝜑 and 𝑧 be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1913, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2480 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb7h 2525* | This version of dfsb7 2275 does not require that 𝜑 and 𝑧 be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1913, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2480 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb10f 2526* | Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑)) | ||
Theorem | sbal1 2527* | Check out sbal 2159 for a version not dependent on ax-13 2371. A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑧 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbal2 2528* | Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022.) (Proof shortened by Wolf Lammen, 23-Sep-2023.) Usage of this theorem is discouraged because it depends on ax-13 2371. Use sbal 2159 instead. (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | 2sb8e 2529* | An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring more disjoint variables, but fewer axioms, see 2sb8ef 2352. (Contributed by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | dfmoeu 2530* | An elementary proof of moeu 2577 in disguise, connecting an expression characterizing uniqueness (df-mo 2534) to that of existential uniqueness (eu6 2568). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2531. (Contributed by Wolf Lammen, 27-May-2019.) |
⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | dfeumo 2531* | An elementary proof showing the reverse direction of dfmoeu 2530. Here the characterizing expression of existential uniqueness (eu6 2568) is derived from that of uniqueness (df-mo 2534). (Contributed by Wolf Lammen, 3-Oct-2023.) |
⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Syntax | wmo 2532 | Extend wff definition to include the at-most-one quantifier ("there exists at most one 𝑥 such that 𝜑"). |
wff ∃*𝑥𝜑 | ||
Theorem | mojust 2533* | Soundness justification theorem for df-mo 2534 (note that 𝑦 and 𝑧 need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). (Contributed by NM, 11-Mar-2010.) Added this theorem by adapting the proof of eujust 2565. (Revised by BJ, 30-Sep-2022.) |
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Definition | df-mo 2534* |
Define the at-most-one quantifier. The expression ∃*𝑥𝜑 is read
"there exists at most one 𝑥 such that 𝜑". This is also
called
the "uniqueness quantifier" but that expression is also used
for the
unique existential quantifier df-eu 2563, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2558. For other possible definitions see moeu 2577 and mo4 2560. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2577, while this definition was then proved as dfmo 2590). (Revised by BJ, 30-Sep-2022.) |
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | nexmo 2535 | Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022.) Avoid ax-11 2154. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | exmo 2536 | Any proposition holds for some 𝑥 or holds for at most one 𝑥. (Contributed by NM, 8-Mar-1995.) Shorten proof and avoid df-eu 2563. (Revised by BJ, 14-Oct-2022.) |
⊢ (∃𝑥𝜑 ∨ ∃*𝑥𝜑) | ||
Theorem | moabs 2537 | Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002.) Shorten proof and avoid df-eu 2563. (Revised by BJ, 14-Oct-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | ||
Theorem | moim 2538 | The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑)) | ||
Theorem | moimi 2539 | The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1913. (Revised by Steven Nguyen, 9-May-2023.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) | ||
Theorem | moimdv 2540* | The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜒 → ∃*𝑥𝜓)) | ||
Theorem | mobi 2541 | Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)) | ||
Theorem | mobii 2542 | Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) Avoid ax-5 1913. (Revised by Wolf Lammen, 24-Sep-2023.) |
⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) | ||
Theorem | mobidv 2543* | Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | mobid 2544 | Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by NM, 8-Mar-1995.) Remove dependency on ax-10 2137, ax-11 2154, ax-13 2371. (Revised by BJ, 14-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | moa1 2545 | If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 1815 and exa1 1840. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∃*𝑥(𝜑 → 𝜓) → ∃*𝑥𝜓) | ||
Theorem | moan 2546 | "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.) |
⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | moani 2547 | "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.) |
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥(𝜓 ∧ 𝜑) | ||
Theorem | moor 2548 | "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.) |
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → ∃*𝑥𝜑) | ||
Theorem | mooran1 2549 | "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ((∃*𝑥𝜑 ∨ ∃*𝑥𝜓) → ∃*𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | mooran2 2550 | "At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → (∃*𝑥𝜑 ∧ ∃*𝑥𝜓)) | ||
Theorem | nfmo1 2551 | Bound-variable hypothesis builder for the at-most-one quantifier. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) Adapt to new definition. (Revised by BJ, 1-Oct-2022.) |
⊢ Ⅎ𝑥∃*𝑥𝜑 | ||
Theorem | nfmod2 2552 | Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 2371. See nfmodv 2553 for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 2371. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid df-eu 2563. (Revised by BJ, 14-Oct-2022.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmodv 2553* | Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod 2555 for a version without disjoint variable conditions but requiring ax-13 2371. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by BJ, 28-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmov 2554* | Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo 2556 for a version without disjoint variable conditions but requiring ax-13 2371. (Contributed by NM, 9-Mar-1995.) (Revised by Wolf Lammen, 2-Oct-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦𝜑 | ||
Theorem | nfmod 2555 | Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo 2556. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfmodv 2553 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmo 2556 | Bound-variable hypothesis builder for the at-most-one quantifier. Note that 𝑥 and 𝑦 need not be disjoint. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfmov 2554 when possible. (Contributed by NM, 9-Mar-1995.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦𝜑 | ||
Theorem | mof 2557* | Version of df-mo 2534 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995.) Extract dfmo 2590 from this proof, and prove mof 2557 from it (as of 30-Sep-2022, directly from df-mo 2534). (Revised by Wolf Lammen, 28-May-2019.) Avoid ax-13 2371. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | mo3 2558* | Alternate definition of the at-most-one quantifier. Definition of [BellMachover] p. 460, except that definition has the side condition that 𝑦 not occur in 𝜑 in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Aug-2019.) Remove dependency on ax-13 2371. (Revised by BJ and WL, 29-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mo 2559* | Equivalent definitions of "there exists at most one". (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Dec-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mo4 2560* |
At-most-one quantifier expressed using implicit substitution. This
theorem is also a direct consequence of mo4f 2561,
but this proof is based
on fewer axioms.
By the way, swapping 𝑥, 𝑦 and 𝜑, 𝜓 leads to an expression for ∃*𝑦𝜓, which is equivalent to ∃*𝑥𝜑 (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 2154. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) | ||
Theorem | mo4f 2561* | At-most-one quantifier expressed using implicit substitution. Note that the disjoint variable condition on 𝑦, 𝜑 can be replaced by the nonfreeness hypothesis ⊢ Ⅎ𝑦𝜑 with essentially the same proof. (Contributed by NM, 10-Apr-2004.) Remove dependency on ax-13 2371. (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) | ||
Syntax | weu 2562 | Extend wff definition to include the unique existential quantifier ("there exists a unique 𝑥 such that 𝜑"). |
wff ∃!𝑥𝜑 | ||
Definition | df-eu 2563 |
Define the existential uniqueness quantifier. This expresses unique
existence, or existential uniqueness, which is the conjunction of
existence (df-ex 1782) and uniqueness (df-mo 2534). The expression
∃!𝑥𝜑 is read "there exists exactly
one 𝑥 such that 𝜑 " or
"there exists a unique 𝑥 such that 𝜑". This is also
called the
"uniqueness quantifier" but that expression is also used for the
at-most-one quantifier df-mo 2534, therefore we avoid that ambiguous name.
Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2606, eu2 2605, eu3v 2564, and eu6 2568. As for double unique existence, beware that the expression ∃!𝑥∃!𝑦𝜑 means "there exists a unique 𝑥 such that there exists a unique 𝑦 such that 𝜑 " which is a weaker property than "there exists exactly one 𝑥 and one 𝑦 such that 𝜑 " (see 2eu4 2650). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2568, while this definition was then proved as dfeu 2589). (Revised by BJ, 30-Sep-2022.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | ||
Theorem | eu3v 2564* | An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Replace a nonfreeness hypothesis with a disjoint variable condition on 𝜑, 𝑦 to reduce axiom usage. (Revised by Wolf Lammen, 29-May-2019.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | eujust 2565* | Soundness justification theorem for eu6 2568 when this was the definition of the unique existential quantifier (note that 𝑦 and 𝑧 need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT 2566 for a proof that provides an example of how it can be achieved through the use of dvelim 2450. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) | ||
Theorem | eujustALT 2566* | Alternate proof of eujust 2565 illustrating the use of dvelim 2450. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) | ||
Theorem | eu6lem 2567* | Lemma of eu6im 2569. A dissection of an idiom characterizing existential uniqueness. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2563 was then proved as dfeu 2589. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))) | ||
Theorem | eu6 2568* | Alternate definition of the unique existential quantifier df-eu 2563 not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2563 was then proved as dfeu 2589. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2154. (Revised by SN, 21-Sep-2023.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | eu6im 2569* | One direction of eu6 2568 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃!𝑥𝜑) | ||
Theorem | euf 2570* | Version of eu6 2568 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2018.) Avoid ax-13 2371. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | euex 2571 | Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.) |
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) | ||
Theorem | eumo 2572 | Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.) |
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | eumoi 2573 | Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
⊢ ∃!𝑥𝜑 ⇒ ⊢ ∃*𝑥𝜑 | ||
Theorem | exmoeub 2574 | Existence implies that uniqueness is equivalent to unique existence. (Contributed by NM, 5-Apr-2004.) |
⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | exmoeu 2575 | Existence is equivalent to uniqueness implying existential uniqueness. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.) |
⊢ (∃𝑥𝜑 ↔ (∃*𝑥𝜑 → ∃!𝑥𝜑)) | ||
Theorem | moeuex 2576 | Uniqueness implies that existence is equivalent to unique existence. (Contributed by BJ, 7-Oct-2022.) |
⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | moeu 2577 | Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995.) This used to be the definition of the at-most-one quantifier, while df-mo 2534 was then proved as dfmo 2590. (Revised by BJ, 30-Sep-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | ||
Theorem | eubi 2578 | Equivalence theorem for the unique existential quantifier. Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) Reduce dependencies on axioms. (Revised by BJ, 7-Oct-2022.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)) | ||
Theorem | eubii 2579 | Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) Avoid ax-5 1913. (Revised by Wolf Lammen, 27-Sep-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) | ||
Theorem | eubidv 2580* | Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | ||
Theorem | eubid 2581 | Formula-building rule for the unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 19-Feb-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | ||
Theorem | nfeu1 2582 | Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2583. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃!𝑥𝜑 | ||
Theorem | nfeu1ALT 2583 | Alternate proof of nfeu1 2582. This illustrates the systematic way of proving nonfreeness in a defined expression: consider the definiens as a tree whose nodes are its subformulas, and prove by tree-induction nonfreeness of each node, starting from the leaves (generally using nfv 1917 or nf* theorems for previously defined expressions) and up to the root. Here, the definiens is a conjunction of two previously defined expressions, which automatically yields the present proof. (Contributed by BJ, 2-Oct-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∃!𝑥𝜑 | ||
Theorem | nfeud2 2584 | Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.) (Proof shortened by BJ, 14-Oct-2022.) Usage of this theorem is discouraged because it depends on ax-13 2371. Use nfeudw 2585 instead. (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeudw 2585* | Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu 2588. Version of nfeud 2586 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 15-Feb-2013.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeud 2586 | Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu 2588. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfeudw 2585 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeuw 2587* | Bound-variable hypothesis builder for the unique existential quantifier. Version of nfeu 2588 with a disjoint variable condition, which does not require ax-13 2371. (Contributed by NM, 8-Mar-1995.) Avoid ax-13 2371. (Revised by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | nfeu 2588 | Bound-variable hypothesis builder for the unique existential quantifier. Note that 𝑥 and 𝑦 need not be disjoint. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker nfeuw 2587 when possible. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | dfeu 2589 | Rederive df-eu 2563 from the old definition eu6 2568. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.) (Proof shortened by BJ, 7-Oct-2022.) (Proof modification is discouraged.) Use df-eu 2563 instead. (New usage is discouraged.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | ||
Theorem | dfmo 2590* | Rederive df-mo 2534 from the old definition moeu 2577. (Contributed by Wolf Lammen, 27-May-2019.) (Proof modification is discouraged.) Use df-mo 2534 instead. (New usage is discouraged.) |
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | euequ 2591* | There exists a unique set equal to a given set. Special case of eueqi 3705 proved using only predicate calculus. The proof needs 𝑦 = 𝑧 be free of 𝑥. This is ensured by having 𝑥 and 𝑦 be distinct. Alternately, a distinctor ¬ ∀𝑥𝑥 = 𝑦 could have been used instead. See eueq 3704 and eueqi 3705 for classes. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023.) |
⊢ ∃!𝑥 𝑥 = 𝑦 | ||
Theorem | sb8eulem 2592* | Lemma. Factor out the common proof skeleton of sb8euv 2593 and sb8eu 2594. Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.) Factor out common proof lines. (Revised by Wolf Lammen, 9-Feb-2023.) |
⊢ Ⅎ𝑦[𝑤 / 𝑥]𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8euv 2593* | Variable substitution in unique existential quantifier. Version of sb8eu 2594 requiring more disjoint variables, but fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8eu 2594 | Variable substitution in unique existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2371. For a version requiring more disjoint variables, but fewer axioms, see sb8euv 2593. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8mo 2595 | Variable substitution for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Alexander van der Vekens, 17-Jun-2017.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | cbvmovw 2596* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvmo 2599 and cbvmow 2597 for versions with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Mar-1995.) (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbvmow 2597* | Rule used to change bound variables, using implicit substitution. Version of cbvmo 2599 with a disjoint variable condition, which does not require ax-10 2137, ax-13 2371. (Contributed by NM, 9-Mar-1995.) (Revised by Gino Giotto, 23-May-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbvmowOLD 2598* | Obsolete version of cbvmow 2597 as of 23-May-2024. (Contributed by NM, 9-Mar-1995.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbvmo 2599 | Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2371. Use the weaker cbvmow 2597, cbvmovw 2596 when possible. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 4-Jan-2023.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbveuvw 2600* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbveu 2603 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 25-Nov-1994.) (Revised by Gino Giotto, 30-Sep-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |