![]() |
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 2582. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu6 2567 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2148 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2317 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1855 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∀wal 1539 ∃wex 1781 Ⅎwnf 1785 ∃!weu 2561 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-10 2137 ax-11 2154 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-nf 1786 df-mo 2533 df-eu 2562 |
This theorem is referenced by: eupicka 2629 2eu8 2653 nfreu1 3407 eusv2i 5385 eusv2nf 5386 reusv2lem3 5391 iota2 6521 sniota 6523 fv3 6896 tz6.12cOLD 6905 eusvobj1 7386 opiota 8027 dfac5lem5 10104 bnj1366 33669 bnj849 33765 pm14.24 42960 eu2ndop1stv 45603 tz6.12c-afv2 45720 setrec2lem2 47385 |
Copyright terms: Public domain | W3C validator |