![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfeu1 | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-eu 2502 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2068 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2192 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1819 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∀wal 1521 ∃wex 1744 Ⅎwnf 1748 ∃!weu 2498 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-11 2074 ax-12 2087 |
This theorem depends on definitions: df-bi 197 df-or 384 df-ex 1745 df-nf 1750 df-eu 2502 |
This theorem is referenced by: nfmo1 2509 eupicka 2566 2eu8 2589 exists2 2591 nfreu1 3139 eusv2i 4893 eusv2nf 4894 reusv2lem3 4901 iota2 5915 sniota 5916 fv3 6244 tz6.12c 6251 eusvobj1 6684 opiota 7273 dfac5lem5 8988 bnj1366 31026 bnj849 31121 pm14.24 38950 eu2ndop1stv 41523 setrec2lem2 42766 |
Copyright terms: Public domain | W3C validator |