![]() |
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 2610. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu6 2594 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2153 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2333 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1855 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∀wal 1537 ∃wex 1782 Ⅎwnf 1786 ∃!weu 2588 |
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 1912 ax-6 1971 ax-7 2016 ax-10 2143 ax-11 2159 ax-12 2176 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-ex 1783 df-nf 1787 df-mo 2558 df-eu 2589 |
This theorem is referenced by: eupicka 2656 2eu8 2681 nfreu1 3286 eusv2i 5256 eusv2nf 5257 reusv2lem3 5262 iota2 6317 sniota 6319 fv3 6669 tz6.12c 6676 eusvobj1 7137 opiota 7754 dfac5lem5 9572 bnj1366 32314 bnj849 32410 pm14.24 41494 eu2ndop1stv 44034 tz6.12c-afv2 44151 setrec2lem2 45574 |
Copyright terms: Public domain | W3C validator |