|   | 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 1909. (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 2544 | . 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒) | 
| 4 | 1 | biimpi 216 | . . 3 ⊢ (𝜓 → 𝜒) | 
| 5 | 4 | moimi 2544 | . 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓) | 
| 6 | 3, 5 | impbii 209 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∃*wmo 2537 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-mo 2539 | 
| This theorem is referenced by: eubii 2584 cbvmo 2603 moanmo 2621 2moswapv 2628 2moswap 2643 nulmo 2712 rmobiia 3385 rmoanidOLD 3391 rmov 3510 euxfr2w 3725 euxfr2 3727 rmoan 3744 reuxfrd 3753 2reu5lem2 3761 2rmoswap 3766 dffun9 6594 funopab 6600 funcnv2 6633 funcnv 6634 fun2cnv 6636 fncnv 6638 imadif 6649 fnres 6694 ov3 7597 oprabex3 8003 brdom6disj 10573 grothprim 10875 axaddf 11186 axmulf 11187 reuxfrdf 32511 rmoun 32514 funcnvmpt 32678 rmoeqi 36189 rmoeqbii 36190 nrmo 36412 alrmomorn 38360 cosscnvssid4 38479 dfeldisj4 38722 disjres 38746 tfsconcatlem 43354 euabsneu 47045 rmotru 48728 oppcthin 49112 indthinc 49134 prsthinc 49136 | 
| Copyright terms: Public domain | W3C validator |