![]() |
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 2612 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 2539 | . 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓))) |
3 | simpl 482 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
4 | 3 | exlimiv 1926 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑) |
5 | 2, 4 | moanimlem 2610 | 1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∃*wmo 2528 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-mo 2530 |
This theorem is referenced by: 2reuswap 3741 2reuswap2 3742 2reu5lem2 3751 2rmoswap 3756 funmo 6568 funmoOLD 6569 funcnv 6622 fncnv 6626 isarep2 6644 fnres 6682 mptfnf 6690 fnopabg 6692 fvopab3ig 7001 opabex 7232 fnoprabg 7543 ovidi 7564 ovig 7567 caovmo 7658 zfrep6 7958 oprabexd 7979 oprabex 7980 nqerf 10953 cnextfun 23967 perfdvf 25831 taylf 26294 reuxfrdf 32288 abrexdomjm 32301 abrexdom 37203 |
Copyright terms: Public domain | W3C validator |