Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > moimi | Structured version Visualization version GIF version |
Description: "At most one" reverses implication. (Contributed by NM, 15-Feb-2006.) |
Ref | Expression |
---|---|
moimi.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
moimi | ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | moim 2507 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑)) | |
2 | moimi.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | mpg 1715 | 1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃*wmo 2459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-eu 2462 df-mo 2463 |
This theorem is referenced by: moa1 2509 moan 2512 moor 2514 mooran1 2515 mooran2 2516 moaneu 2521 2moex 2531 2euex 2532 2exeu 2537 sndisj 4574 disjxsn 4576 fununmo 5847 funcnvsn 5850 nfunsn 6135 caovmo 6769 iunmapdisj 8729 brdom3 9231 brdom5 9232 brdom4 9233 nqerf 9631 shftfn 13661 2ndcdisj2 21070 plyexmo 23872 ajfuni 27099 funadj 28129 cnlnadjeui 28320 |
Copyright terms: Public domain | W3C validator |