![]() |
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 "at most one" quantifier (inference rule). (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 | mobii.1 | . . . 4 ⊢ (𝜓 ↔ 𝜒) | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒)) |
3 | 2 | mobidv 2639 | . 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
4 | 3 | trud 1641 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1632 ∃*wmo 2619 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-tru 1634 df-ex 1853 df-nf 1858 df-eu 2622 df-mo 2623 |
This theorem is referenced by: moanmo 2681 2moswap 2696 rmobiia 3281 rmov 3374 euxfr2 3543 rmoan 3558 2reu5lem2 3566 reuxfr2d 5019 dffun9 6060 funopab 6066 funcnv2 6097 funcnv 6098 fun2cnv 6100 fncnv 6102 imadif 6113 fnres 6147 ov3 6944 oprabex3 7304 brdom6disj 9556 grothprim 9858 axaddf 10168 axmulf 10169 reuxfr3d 29668 funcnvmptOLD 29807 funcnvmpt 29808 alrmomorn 34465 cosscnvssid4 34569 2rmoswap 41704 |
Copyright terms: Public domain | W3C validator |