Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mobii | 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 9 | . . 3 ⊢ (⊤ → (𝜓 ↔ 𝜒)) |
3 | 2 | mobidv 1936 | . 2 ⊢ (⊤ → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) |
4 | 3 | trud 1252 | 1 ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 ⊤wtru 1244 ∃*wmo 1901 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-tru 1246 df-nf 1350 df-eu 1903 df-mo 1904 |
This theorem is referenced by: moaneu 1976 moanmo 1977 2moswapdc 1990 2exeu 1992 rmobiia 2499 rmov 2574 euxfr2dc 2726 rmoan 2739 2rmorex 2745 mosn 3406 dffun9 4930 funopab 4935 funco 4940 funcnv2 4959 funcnv 4960 fun2cnv 4963 fncnv 4965 imadif 4979 fnres 5015 ovi3 5637 oprabex3 5756 frecuzrdgfn 9198 |
Copyright terms: Public domain | W3C validator |