![]() |
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 "at most one" quantifier. (Contributed by NM, 23-Mar-1995.) |
Ref | Expression |
---|---|
moanimv | ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1995 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | moanim 2678 | 1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 ∃*wmo 2619 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-10 2174 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-ex 1853 df-nf 1858 df-eu 2622 df-mo 2623 |
This theorem is referenced by: 2reuswap 3562 2reu5lem2 3566 funmo 6047 funcnv 6098 fncnv 6102 isarep2 6118 fnres 6147 mptfnf 6155 fnopabg 6157 fvopab3ig 6420 opabex 6627 fnoprabg 6908 ovidi 6926 ovig 6929 caovmo 7018 zfrep6 7281 oprabexd 7302 oprabex 7303 nqerf 9954 cnextfun 22088 perfdvf 23887 taylf 24335 2reuswap2 29667 abrexdomjm 29683 abrexdom 33857 2rmoswap 41704 |
Copyright terms: Public domain | W3C validator |