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 1905. (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 230 | . . 3 ⊢ (𝜒 → 𝜓) |
3 | 2 | moimi 2621 | . 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒) |
4 | 1 | biimpi 218 | . . 3 ⊢ (𝜓 → 𝜒) |
5 | 4 | moimi 2621 | . 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓) |
6 | 3, 5 | impbii 211 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∃*wmo 2614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 209 df-ex 1775 df-mo 2616 |
This theorem is referenced by: eubii 2664 cbvmow 2682 cbvmo 2683 moanmo 2701 2moswapv 2708 2moswap 2723 nulmo 2796 rmoanid 3327 rmobiia 3394 rmov 3521 euxfr2w 3709 euxfr2 3711 rmoan 3728 reuxfrd 3737 2reu5lem2 3745 2rmoswap 3750 dffun9 6377 funopab 6383 funcnv2 6415 funcnv 6416 fun2cnv 6418 fncnv 6420 imadif 6431 fnres 6467 ov3 7303 oprabex3 7670 brdom6disj 9946 grothprim 10248 axaddf 10559 axmulf 10560 reuxfrdf 30247 rmoun 30250 funcnvmpt 30404 nrmo 33751 alrmomorn 35604 cosscnvssid4 35709 dfeldisj4 35945 euabsneu 43254 |
Copyright terms: Public domain | W3C validator |