![]() |
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. See also nfeu1ALT 2584. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu6 2569 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2149 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2318 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wal 1540 ∃wex 1782 Ⅎwnf 1786 ∃!weu 2563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-10 2138 ax-11 2155 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-nf 1787 df-mo 2535 df-eu 2564 |
This theorem is referenced by: eupicka 2631 2eu8 2655 nfreu1 3409 eusv2i 5393 eusv2nf 5394 reusv2lem3 5399 iota2 6533 sniota 6535 fv3 6910 tz6.12cOLD 6919 eusvobj1 7402 opiota 8045 dfac5lem5 10122 bnj1366 33840 bnj849 33936 pm14.24 43191 eu2ndop1stv 45833 tz6.12c-afv2 45950 setrec2lem2 47739 |
Copyright terms: Public domain | W3C validator |