![]() |
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 1892. (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 229 | . . 3 ⊢ (𝜒 → 𝜓) |
3 | 2 | moimi 2583 | . 2 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜒) |
4 | 1 | biimpi 217 | . . 3 ⊢ (𝜓 → 𝜒) |
5 | 4 | moimi 2583 | . 2 ⊢ (∃*𝑥𝜒 → ∃*𝑥𝜓) |
6 | 3, 5 | impbii 210 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∃*wmo 2576 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 |
This theorem depends on definitions: df-bi 208 df-ex 1766 df-mo 2578 |
This theorem is referenced by: eubii 2632 cbvmo 2656 moanmo 2678 2moswapv 2686 2moswap 2701 nulmo 2776 rmoanid 3292 rmobiia 3357 rmov 3468 euxfr2 3652 rmoan 3669 reuxfrd 3678 2reu5lem2 3686 2rmoswap 3691 dffun9 6261 funopab 6267 funcnv2 6299 funcnv 6300 fun2cnv 6302 fncnv 6304 imadif 6315 fnres 6351 ov3 7174 oprabex3 7541 brdom6disj 9807 grothprim 10109 axaddf 10420 axmulf 10421 reuxfrdf 29943 rmoun 29946 funcnvmpt 30098 nrmo 33369 alrmomorn 35165 cosscnvssid4 35269 dfeldisj4 35505 euabsneu 42801 |
Copyright terms: Public domain | W3C validator |