| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mobii | Structured version Visualization version GIF version | ||
| Description: Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) Avoid ax-5 1911. (Revised by Wolf Lammen, 24-Sep-2023.) |
| Ref | Expression |
|---|---|
| mobii.1 | ⊢ (𝜓 ↔ 𝜒) |
| Ref | Expression |
|---|---|
| mobii | ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mobii.1 | . . . 4 ⊢ (𝜓 ↔ 𝜒) | |
| 2 | 1 | biimpri 228 | . . 3 ⊢ (𝜒 → 𝜓) |
| 3 | 2 | moimi 2542 | . 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒) |
| 4 | 1 | biimpi 216 | . . 3 ⊢ (𝜓 → 𝜒) |
| 5 | 4 | moimi 2542 | . 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓) |
| 6 | 3, 5 | impbii 209 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∃*wmo 2535 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
| This theorem depends on definitions: df-bi 207 df-ex 1781 df-mo 2537 |
| This theorem is referenced by: eubii 2582 cbvmo 2601 moanmo 2619 2moswapv 2626 2moswap 2641 nulmo 2710 rmobiia 3354 rmov 3468 euxfr2w 3676 euxfr2 3678 rmoan 3695 reuxfrd 3704 2reu5lem2 3712 2rmoswap 3717 dffun9 6518 funopab 6524 funcnv2 6557 funcnv 6558 fun2cnv 6560 fncnv 6562 imadif 6573 fnres 6616 ov3 7518 oprabex3 7918 brdom6disj 10433 grothprim 10735 axaddf 11046 axmulf 11047 reuxfrdf 32481 rmoun 32484 funcnvmpt 32660 rmoeqi 36242 rmoeqbii 36243 nrmo 36465 alrmomorn 38400 cosscnvssid4 38589 dfeldisj4 38828 disjres 38852 tfsconcatlem 43443 sinnpoly 47005 euabsneu 47142 rmotru 48917 oppcthin 49553 indthinc 49577 prsthinc 49579 |
| Copyright terms: Public domain | W3C validator |