![]() |
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 2628 | . 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
4 | 3 | trud 1642 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1633 ∃*wmo 2608 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-12 2196 |
This theorem depends on definitions: df-bi 197 df-tru 1635 df-ex 1854 df-nf 1859 df-eu 2611 df-mo 2612 |
This theorem is referenced by: moanmo 2670 2moswap 2685 rmobiia 3271 rmov 3362 euxfr2 3532 rmoan 3547 2reu5lem2 3555 reuxfr2d 5040 dffun9 6078 funopab 6084 funcnv2 6118 funcnv 6119 fun2cnv 6121 fncnv 6123 imadif 6134 fnres 6168 ov3 6963 oprabex3 7323 brdom6disj 9566 grothprim 9868 axaddf 10178 axmulf 10179 reuxfr3d 29658 funcnvmptOLD 29797 funcnvmpt 29798 alrmomorn 34464 cosscnvssid4 34568 2rmoswap 41708 |
Copyright terms: Public domain | W3C validator |