![]() |
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 1914. (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 227 | . . 3 ⊢ (𝜒 → 𝜓) |
3 | 2 | moimi 2540 | . 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒) |
4 | 1 | biimpi 215 | . . 3 ⊢ (𝜓 → 𝜒) |
5 | 4 | moimi 2540 | . 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓) |
6 | 3, 5 | impbii 208 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∃*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: eubii 2580 cbvmowOLD 2599 cbvmo 2600 moanmo 2619 2moswapv 2626 2moswap 2641 nulmo 2709 rmobiia 3383 rmoanidOLD 3389 rmov 3502 euxfr2w 3714 euxfr2 3716 rmoan 3733 reuxfrd 3742 2reu5lem2 3750 2rmoswap 3755 dffun9 6569 funopab 6575 funcnv2 6608 funcnv 6609 fun2cnv 6611 fncnv 6613 imadif 6624 fnres 6667 ov3 7557 oprabex3 7951 brdom6disj 10514 grothprim 10816 axaddf 11127 axmulf 11128 reuxfrdf 31696 rmoun 31699 funcnvmpt 31861 nrmo 35200 alrmomorn 37133 cosscnvssid4 37253 dfeldisj4 37496 disjres 37520 tfsconcatlem 41957 euabsneu 45611 rmotru 47329 oppcthin 47499 indthinc 47512 prsthinc 47514 |
Copyright terms: Public domain | W3C validator |