Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mo4 | Structured version Visualization version 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 1830 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | mo4.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | mo4f 2504 | 1 ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∀wal 1473 ∃*wmo 2459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 |
This theorem is referenced by: eu4 2506 rmo4 3366 dffun3 5815 fun11 5877 brprcneu 6096 dff13 6416 mpt2fun 6660 caovmo 6769 wemoiso 7044 wemoiso2 7045 addsrmo 9773 mulsrmo 9774 summo 14295 prodmo 14505 hausflimi 21594 vitalilem3 23185 plyexmo 23872 tglineintmo 25337 frg2wot1 26584 ajmoi 27098 pjhthmo 27545 adjmo 28075 moel 28707 funtransport 31308 funray 31417 funline 31419 lineintmo 31434 dffrege115 37292 frgr2wwlk1 41494 |
Copyright terms: Public domain | W3C validator |