![]() |
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 2603 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2169 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2293 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1920 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∀wal 1622 ∃wex 1845 Ⅎwnf 1849 ∃!weu 2599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-10 2160 ax-11 2175 ax-12 2188 |
This theorem depends on definitions: df-bi 197 df-or 384 df-ex 1846 df-nf 1851 df-eu 2603 |
This theorem is referenced by: nfmo1 2610 eupicka 2667 2eu8 2690 exists2 2692 nfreu1 3240 eusv2i 5004 eusv2nf 5005 reusv2lem3 5012 iota2 6030 sniota 6031 fv3 6359 tz6.12c 6366 eusvobj1 6799 opiota 7388 dfac5lem5 9132 bnj1366 31199 bnj849 31294 pm14.24 39127 eu2ndop1stv 41700 setrec2lem2 42943 |
Copyright terms: Public domain | W3C validator |