| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > moanimv | Structured version Visualization version GIF version | ||
| Description: Introduction of a conjunct into an at-most-one quantifier. Version of moanim 2620 requiring disjoint variables, but fewer axioms. (Contributed by NM, 23-Mar-1995.) Reduce axiom usage . (Revised by Wolf Lammen, 8-Feb-2023.) |
| Ref | Expression |
|---|---|
| moanimv | ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ibar 528 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
| 2 | 1 | mobidv 2549 | . 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓))) |
| 3 | simpl 482 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
| 4 | 3 | exlimiv 1930 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑) |
| 5 | 2, 4 | moanimlem 2618 | 1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∃*wmo 2538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-mo 2540 |
| This theorem is referenced by: 2reuswap 3752 2reuswap2 3753 2reu5lem2 3762 2rmoswap 3767 funmo 6581 funmoOLD 6582 funcnv 6635 fncnv 6639 isarep2 6658 fnres 6695 mptfnf 6703 fnopabg 6705 fvopab3ig 7012 opabex 7240 fnoprabg 7556 ovidi 7576 ovig 7579 caovmo 7670 zfrep6 7979 oprabexd 8000 oprabex 8001 nqerf 10970 cnextfun 24072 perfdvf 25938 taylf 26402 reuxfrdf 32510 abrexdomjm 32526 abrexdom 37737 modelaxreplem2 44996 |
| Copyright terms: Public domain | W3C validator |