| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > moimi | Structured version Visualization version GIF version | ||
| Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1910. (Revised by Steven Nguyen, 9-May-2023.) |
| Ref | Expression |
|---|---|
| moimi.1 | ⊢ (𝜑 → 𝜓) |
| Ref | Expression |
|---|---|
| moimi | ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moimi.1 | . . . . 5 ⊢ (𝜑 → 𝜓) | |
| 2 | 1 | imim1i 63 | . . . 4 ⊢ ((𝜓 → 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦)) |
| 3 | 2 | alimi 1811 | . . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
| 4 | 3 | eximi 1835 | . 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
| 5 | df-mo 2540 | . 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦)) | |
| 6 | df-mo 2540 | . 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
| 7 | 4, 5, 6 | 3imtr4i 292 | 1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∃wex 1779 ∃*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 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-mo 2540 |
| This theorem is referenced by: mobii 2548 moa1 2551 moan 2552 moor 2554 mooran1 2555 mooran2 2556 moaneu 2623 2moexv 2627 2euexv 2631 2exeuv 2632 2moex 2640 2euex 2641 2exeu 2646 sndisj 5135 disjxsn 5137 axsepgfromrep 5294 fununmo 6613 funcnvsn 6616 nfunsn 6948 caovmo 7670 iunmapdisj 10063 brdom3 10568 brdom5 10569 brdom4 10570 nqerf 10970 shftfn 15112 2ndcdisj2 23465 plyexmo 26355 ajfuni 30878 funadj 31905 cnlnadjeui 32096 amosym1 36427 funressnvmo 47057 |
| Copyright terms: Public domain | W3C validator |