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 2491 | . 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
4 | 3 | trud 1493 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1484 ∃*wmo 2471 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-tru 1486 df-ex 1705 df-nf 1710 df-eu 2474 df-mo 2475 |
This theorem is referenced by: moanmo 2532 2moswap 2547 rmobiia 3132 rmov 3222 euxfr2 3391 rmoan 3406 2reu5lem2 3414 reuxfr2d 4891 dffun9 5917 funopab 5923 funcnv2 5957 funcnv 5958 fun2cnv 5960 fncnv 5962 imadif 5973 fnres 6007 ov3 6797 oprabex3 7157 brdom6disj 9354 grothprim 9656 axaddf 9966 axmulf 9967 reuxfr3d 29329 funcnvmptOLD 29467 funcnvmpt 29468 alrmomo 34123 2rmoswap 41184 |
Copyright terms: Public domain | W3C validator |