Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mo4 | GIF version |
Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
Ref | Expression |
---|---|
mo4.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
mo4 | ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1493 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | mo4.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | mo4f 2037 | 1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∀wal 1314 ∃*wmo 1978 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-eu 1980 df-mo 1981 |
This theorem is referenced by: eu4 2039 rmo4 2850 dffun5r 5105 dffun6f 5106 fun11 5160 brprcneu 5382 dff13 5637 mpofun 5841 caovimo 5932 th3qlem1 6499 addnq0mo 7223 mulnq0mo 7224 addsrmo 7519 mulsrmo 7520 summodc 11120 limcimo 12730 |
Copyright terms: Public domain | W3C validator |