Home | Metamath
Proof Explorer Theorem List (p. 27 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfsb4ALT 2601 | Alternate version of nfsb4 2536. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝜃) | ||
Theorem | sbi1ALT 2602 | Alternate version of sbi1 2067. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) ⇒ ⊢ (𝜂 → (𝜃 → 𝜏)) | ||
Theorem | sbi2ALT 2603 | Alternate version of sbi2 2302. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) ⇒ ⊢ ((𝜃 → 𝜏) → 𝜂) | ||
Theorem | sbimALT 2604 | Alternate version of sbim 2303. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) ⇒ ⊢ (𝜂 ↔ (𝜃 → 𝜏)) | ||
Theorem | sbrimALT 2605 | Alternate version of sbrim 2305. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 → 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 → 𝜓)))) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜂 ↔ (𝜑 → 𝜏)) | ||
Theorem | sbanALT 2606 | Alternate version of sban 2077. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 ∧ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 ∧ 𝜓)))) ⇒ ⊢ (𝜂 ↔ (𝜃 ∧ 𝜏)) | ||
Theorem | sbbiALT 2607 | Alternate version of sbbi 2309. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 ↔ 𝜓)))) ⇒ ⊢ (𝜂 ↔ (𝜃 ↔ 𝜏)) | ||
Theorem | sblbisALT 2608 | Alternate version of sblbis 2311. (Contributed by NM, 19-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜂 ↔ ((𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ∧ ∃𝑥(𝑥 = 𝑦 ∧ (𝜑 ↔ 𝜓)))) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜂 ↔ (𝜃 ↔ 𝜒)) | ||
Theorem | sbieALT 2609 | Alternate version of sbie 2540. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝜃 ↔ 𝜓) | ||
Theorem | sbiedALT 2610 | Alternate version of sbied 2541. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜒)) | ||
Theorem | sbco2ALT 2611 | Alternate version of sbco2 2549. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑧 = 𝑦 → ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) ∧ ∃𝑧(𝑧 = 𝑦 ∧ ((𝑥 = 𝑧 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))))) & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (𝜏 ↔ 𝜃) | ||
Theorem | sb7fALT 2612* | Alternate version of sb7f 2564. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (𝜃 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | dfsb7ALT 2613* | Alternate version of dfsb7 2277. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | dfmoeu 2614* | An elementary proof of moeu 2664 in disguise, connecting an expression characterizing uniqueness (df-mo 2618) to that of existential uniqueness (eu6 2655). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2615. (Contributed by Wolf Lammen, 27-May-2019.) |
⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | dfeumo 2615* | An elementary proof showing the reverse direction of dfmoeu 2614. Here the characterizing expression of existential uniqueness (eu6 2655) is derived from that of uniqueness (df-mo 2618). (Contributed by Wolf Lammen, 3-Oct-2023.) |
⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Syntax | wmo 2616 | Extend wff definition to include the at-most-one quantifier ("there exists at most one 𝑥 such that 𝜑"). |
wff ∃*𝑥𝜑 | ||
Theorem | mojust 2617* | Soundness justification theorem for df-mo 2618 (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 2652. (Revised by BJ, 30-Sep-2022.) |
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Definition | df-mo 2618* |
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 2650, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460, whose definition we show as mo3 2644. For other possible definitions see moeu 2664 and mo4 2646. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2664, while this definition was then proved as dfmo 2678). (Revised by BJ, 30-Sep-2022.) |
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | nexmo 2619 | Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022.) Avoid ax-11 2151. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | exmo 2620 | Any proposition holds for some 𝑥 or holds for at most one 𝑥. (Contributed by NM, 8-Mar-1995.) Shorten proof and avoid df-eu 2650. (Revised by BJ, 14-Oct-2022.) |
⊢ (∃𝑥𝜑 ∨ ∃*𝑥𝜑) | ||
Theorem | moabs 2621 | Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002.) Shorten proof and avoid df-eu 2650. (Revised by BJ, 14-Oct-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | ||
Theorem | moim 2622 | The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑)) | ||
Theorem | moimi 2623 | The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1902. (Revised by Steven Nguyen, 9-May-2023.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) | ||
Theorem | moimiOLD 2624 | Obsolete version of moimi 2623 as of 9-May-2023. The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) | ||
Theorem | moimdv 2625* | The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜒 → ∃*𝑥𝜓)) | ||
Theorem | mobi 2626 | Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.) |
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓)) | ||
Theorem | mobii 2627 | 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 1902. (Revised by Wolf Lammen, 24-Sep-2023.) |
⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) | ||
Theorem | mobiiOLD 2628 | Obsolete version of mobii 2627 as of 24-Sep-2023. (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) | ||
Theorem | mobidv 2629* | 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 2630 | Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by NM, 8-Mar-1995.) Remove dependency on ax-10 2136, ax-11 2151, ax-13 2383. (Revised by BJ, 14-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | moa1 2631 | If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 1805 and exa1 1829. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∃*𝑥(𝜑 → 𝜓) → ∃*𝑥𝜓) | ||
Theorem | moan 2632 | "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.) |
⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑)) | ||
Theorem | moani 2633 | "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.) |
⊢ ∃*𝑥𝜑 ⇒ ⊢ ∃*𝑥(𝜓 ∧ 𝜑) | ||
Theorem | moor 2634 | "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.) |
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → ∃*𝑥𝜑) | ||
Theorem | mooran1 2635 | "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ ((∃*𝑥𝜑 ∨ ∃*𝑥𝜓) → ∃*𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | mooran2 2636 | "At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → (∃*𝑥𝜑 ∧ ∃*𝑥𝜓)) | ||
Theorem | nfmo1 2637 | 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 2638 | Bound-variable hypothesis builder for the at-most-one quantifier. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid df-eu 2650. (Revised by BJ, 14-Oct-2022.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmodv 2639* | Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod 2641 for a version without disjoint variable conditions but requiring ax-13 2383. (Contributed by BJ, 28-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmov 2640* | Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo 2642 for a version without disjoint variable conditions but requiring ax-13 2383. (Contributed by Wolf Lammen, 2-Oct-2023.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦𝜑 | ||
Theorem | nfmod 2641 | Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo 2642. (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfmo 2642 | Bound-variable hypothesis builder for the at-most-one quantifier. Note that 𝑥 and 𝑦 need not be disjoint. (Contributed by NM, 9-Mar-1995.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦𝜑 | ||
Theorem | mof 2643* | Version of df-mo 2618 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995.) Extract dfmo 2678 from this proof, and prove mof 2643 from it (as of 30-Sep-2022, directly from df-mo 2618). (Revised by Wolf Lammen, 28-May-2019.) Avoid ax-13 2383. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | mo3 2644* | 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 2383. (Revised by BJ and WL, 29-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mo 2645* | 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 2646* |
At-most-one quantifier expressed using implicit substitution. This
theorem is also a direct consequence of mo4f 2647,
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 2151. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) | ||
Theorem | mo4f 2647* | 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 2383. (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) | ||
Theorem | mo4OLD 2648* | Obsolete version of mo4 2646 as of 18-Oct-2023. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) | ||
Syntax | weu 2649 | Extend wff definition to include the unique existential quantifier ("there exists a unique 𝑥 such that 𝜑"). |
wff ∃!𝑥𝜑 | ||
Definition | df-eu 2650 |
Define the existential uniqueness quantifier. This expresses unique
existence, or existential uniqueness, which is the conjunction of
existence (df-ex 1772) and uniqueness (df-mo 2618). 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 2618, 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 2690, eu2 2689, eu3v 2651, and eu6 2655. 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 2737). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2655, while this definition was then proved as dfeu 2677). (Revised by BJ, 30-Sep-2022.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | ||
Theorem | eu3v 2651* | 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 2652* | Soundness justification theorem for eu6 2655 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 2653 for a proof that provides an example of how it can be achieved through the use of dvelim 2468. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) | ||
Theorem | eujustALT 2653* | Alternate proof of eujust 2652 illustrating the use of dvelim 2468. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) | ||
Theorem | eu6lem 2654* | Lemma of eu6im 2656. 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 2650 was then proved as dfeu 2677. (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 2655* | Alternate definition of the unique existential quantifier df-eu 2650 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 2650 was then proved as dfeu 2677. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2151. (Revised by SN, 21-Sep-2023.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | eu6im 2656* | One direction of eu6 2655 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃!𝑥𝜑) | ||
Theorem | euf 2657* | Version of eu6 2655 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 2383. (Revised by Wolf Lammen, 16-Oct-2022.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | euex 2658 | 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 2659 | Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.) |
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | eumoi 2660 | Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
⊢ ∃!𝑥𝜑 ⇒ ⊢ ∃*𝑥𝜑 | ||
Theorem | exmoeub 2661 | Existence implies that uniqueness is equivalent to unique existence. (Contributed by NM, 5-Apr-2004.) |
⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | exmoeu 2662 | 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 2663 | Uniqueness implies that existence is equivalent to unique existence. (Contributed by BJ, 7-Oct-2022.) |
⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | moeu 2664 | 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 2618 was then proved as dfmo 2678. (Revised by BJ, 30-Sep-2022.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | ||
Theorem | eubi 2665 | 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 2666 | 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 1902. (Revised by Wolf Lammen, 27-Sep-2023.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) | ||
Theorem | eubiiOLD 2667 | Obsolete version of eubii 2666 as of 27-Sep-2023. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) | ||
Theorem | eubidv 2668* | 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 2669 | 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 2670 | Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2671. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃!𝑥𝜑 | ||
Theorem | nfeu1ALT 2671 | Alternate proof of nfeu1 2670. 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 1906 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 2672 | 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.) |
⊢ Ⅎ𝑦𝜑 & ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeudw 2673* | Version of nfeud 2674 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeud 2674 | Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu 2676. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeuw 2675* | Version of nfeu 2676 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | nfeu 2676 | Bound-variable hypothesis builder for the unique existential quantifier. Note that 𝑥 and 𝑦 need not be disjoint. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | dfeu 2677 | Rederive df-eu 2650 from the old definition eu6 2655. (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 2650 instead. (New usage is discouraged.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | ||
Theorem | dfmo 2678* | Rederive df-mo 2618 from the old definition moeu 2664. (Contributed by Wolf Lammen, 27-May-2019.) (Proof modification is discouraged.) Use df-mo 2618 instead. (New usage is discouraged.) |
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | euequ 2679* | There exists a unique set equal to a given set. Special case of eueqi 3699 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 3698 and eueqi 3699 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 2680* | Lemma. Factor out the common proof skeleton of sb8euv 2681 and sb8eu 2682. 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 2681* | Variable substitution in unique existential quantifier. Version of sb8eu 2682 requiring more disjoint variables, but fewer axioms. (Contributed by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8eu 2682 | Variable substitution in unique existential quantifier. For a version requiring more disjoint variables, but fewer axioms, see sb8euv 2681. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8mo 2683 | Variable substitution for the at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | cbvmow 2684* | Version of cbvmo 2685 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbvmo 2685 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 4-Jan-2023.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | cbveuw 2686* | Version of cbveu 2687 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by Gino Giotto, 10-Jan-2024.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓) | ||
Theorem | cbveu 2687 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓) | ||
Theorem | cbveuALT 2688 | Alternative proof of cbveu 2687. Since df-eu 2650 combines two other quantifiers, one can base this theorem on their associated 'change bounded variable' kind of theorems as well. (Contributed by Wolf Lammen, 5-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓) | ||
Theorem | eu2 2689* | An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.) (Proof shortened by Wolf Lammen, 2-Dec-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | eu1 2690* | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 29-Oct-2018.) Avoid ax-13 2383. (Revised by Wolf Lammen, 7-Feb-2023.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) | ||
Theorem | euor 2691 | Introduce a disjunct into a unique existential quantifier. For a version requiring disjoint variables, but fewer axioms, see euorv 2692. (Contributed by NM, 21-Oct-2005.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | euorv 2692* | Introduce a disjunct into a unique existential quantifier. Version of euor 2691 requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023.) |
⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | euor2 2693 | Introduce or eliminate a disjunct in a unique existential quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 27-Dec-2018.) |
⊢ (¬ ∃𝑥𝜑 → (∃!𝑥(𝜑 ∨ 𝜓) ↔ ∃!𝑥𝜓)) | ||
Theorem | sbmo 2694* | Substitution into an at-most-one quantifier. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ([𝑦 / 𝑥]∃*𝑧𝜑 ↔ ∃*𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | eu4 2695* | Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) | ||
Theorem | euimmo 2696 | Existential uniqueness implies uniqueness through reverse implication. (Contributed by NM, 22-Apr-1995.) |
⊢ (∀𝑥(𝜑 → 𝜓) → (∃!𝑥𝜓 → ∃*𝑥𝜑)) | ||
Theorem | euim 2697 | Add unique existential quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Proof shortened by Wolf Lammen, 1-Oct-2023.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (∃!𝑥𝜓 → ∃!𝑥𝜑)) | ||
Theorem | euimOLD 2698 | Obsolete version of euim 2697 as of 1-Oct-2023. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((∃𝑥𝜑 ∧ ∀𝑥(𝜑 → 𝜓)) → (∃!𝑥𝜓 → ∃!𝑥𝜑)) | ||
Theorem | moanimlem 2699 | Factor out the common proof skeleton of moanimv 2700 and moanim 2701. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 24-Dec-2018.) Factor out common proof lines. (Revised by Wolf Lammen, 8-Feb-2023.) |
⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓))) & ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑) ⇒ ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) | ||
Theorem | moanimv 2700* | Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2701 requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023.) |
⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |