![]() |
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 2708 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 524 | . . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
2 | 1 | mobidv 2617 | . 2 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥(𝜑 ∧ 𝜓))) |
3 | simpl 476 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑) | |
4 | 3 | exlimiv 2029 | . 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → 𝜑) |
5 | 2, 4 | moanimlem 2706 | 1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∃*wmo 2603 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-mo 2605 |
This theorem is referenced by: 2reuswap 3637 2reu5lem2 3641 funmo 6143 funcnv 6195 fncnv 6199 isarep2 6215 fnres 6244 mptfnf 6252 fnopabg 6254 fvopab3ig 6529 opabex 6744 fnoprabg 7026 ovidi 7044 ovig 7047 caovmo 7136 zfrep6 7401 oprabexd 7420 oprabex 7421 nqerf 10074 cnextfun 22245 perfdvf 24073 taylf 24521 2reuswap2 29877 abrexdomjm 29889 abrexdom 34063 2rmoswap 42003 |
Copyright terms: Public domain | W3C validator |