![]() |
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 1913. (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 1837 | . 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
5 | df-mo 2538 | . 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦)) | |
6 | df-mo 2538 | . 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
7 | 4, 5, 6 | 3imtr4i 291 | 1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ∃wex 1781 ∃*wmo 2536 |
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 206 df-ex 1782 df-mo 2538 |
This theorem is referenced by: mobii 2546 moa1 2549 moan 2550 moor 2552 mooran1 2553 mooran2 2554 moaneu 2623 2moexv 2627 2euexv 2631 2exeuv 2632 2moex 2640 2euex 2641 2exeu 2646 sndisj 5094 disjxsn 5096 axsepgfromrep 5252 fununmo 6545 funcnvsn 6548 nfunsn 6881 caovmo 7585 iunmapdisj 9917 brdom3 10422 brdom5 10423 brdom4 10424 nqerf 10824 shftfn 14912 2ndcdisj2 22754 plyexmo 25619 ajfuni 29646 funadj 30673 cnlnadjeui 30864 amosym1 34830 funressnvmo 45174 |
Copyright terms: Public domain | W3C validator |