![]() |
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 1914. (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 1814 | . . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦)) |
4 | 3 | eximi 1838 | . 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) |
5 | df-mo 2535 | . 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦)) | |
6 | df-mo 2535 | . 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | |
7 | 4, 5, 6 | 3imtr4i 292 | 1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∃wex 1782 ∃*wmo 2533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-mo 2535 |
This theorem is referenced by: mobii 2543 moa1 2546 moan 2547 moor 2549 mooran1 2550 mooran2 2551 moaneu 2620 2moexv 2624 2euexv 2628 2exeuv 2629 2moex 2637 2euex 2638 2exeu 2643 sndisj 5140 disjxsn 5142 axsepgfromrep 5298 fununmo 6596 funcnvsn 6599 nfunsn 6934 caovmo 7644 iunmapdisj 10018 brdom3 10523 brdom5 10524 brdom4 10525 nqerf 10925 shftfn 15020 2ndcdisj2 22961 plyexmo 25826 ajfuni 30112 funadj 31139 cnlnadjeui 31330 amosym1 35311 funressnvmo 45755 |
Copyright terms: Public domain | W3C validator |