![]() |
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 1911. (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 1813 | . . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
4 | 3 | eximi 1836 | . 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
5 | df-mo 2598 | . 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦)) | |
6 | df-mo 2598 | . 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
7 | 4, 5, 6 | 3imtr4i 295 | 1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 ∃wex 1781 ∃*wmo 2596 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-ex 1782 df-mo 2598 |
This theorem is referenced by: mobii 2606 moa1 2610 moan 2611 moor 2613 mooran1 2614 mooran2 2615 moaneu 2685 2moexv 2689 2euexv 2693 2exeuv 2694 2moex 2702 2euex 2703 2exeu 2708 sndisj 5021 disjxsn 5023 axsepgfromrep 5165 fununmo 6371 funcnvsn 6374 nfunsn 6682 caovmo 7365 iunmapdisj 9434 brdom3 9939 brdom5 9940 brdom4 9941 nqerf 10341 shftfn 14424 2ndcdisj2 22062 plyexmo 24909 ajfuni 28642 funadj 29669 cnlnadjeui 29860 funressnvmo 43637 |
Copyright terms: Public domain | W3C validator |