| 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.) |
| Ref | Expression |
|---|---|
| mobii.1 | ⊢ (𝜓 ↔ 𝜒) |
| Ref | Expression |
|---|---|
| mobii | ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mobi 2547 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | |
| 2 | mobii.1 | . 2 ⊢ (𝜓 ↔ 𝜒) | |
| 3 | 1, 2 | mpg 1798 | 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 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1781 df-mo 2539 |
| This theorem is referenced by: cbvmo 2604 moanmo 2622 2moswapv 2629 2moswap 2644 nulmo 2713 rmobiia 3356 rmov 3470 euxfr2w 3678 euxfr2 3680 rmoan 3697 reuxfrd 3706 2reu5lem2 3714 2rmoswap 3719 dffun9 6521 funopab 6527 funcnv2 6560 funcnv 6561 fun2cnv 6563 fncnv 6565 imadif 6576 fnres 6619 ov3 7521 oprabex3 7921 brdom6disj 10442 grothprim 10745 axaddf 11056 axmulf 11057 reuxfrdf 32565 rmoun 32568 funcnvmpt 32745 rmoeqi 36381 rmoeqbii 36382 nrmo 36604 alrmomorn 38551 cosscnvssid4 38740 dfeldisj4 38979 disjres 39003 tfsconcatlem 43578 sinnpoly 47137 euabsneu 47274 rmotru 49048 oppcthin 49683 indthinc 49707 prsthinc 49709 |
| Copyright terms: Public domain | W3C validator |