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 2668. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu6 2652 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2146 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2334 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1844 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∀wal 1526 ∃wex 1771 Ⅎwnf 1775 ∃!weu 2646 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-10 2136 ax-11 2151 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ex 1772 df-nf 1776 df-mo 2615 df-eu 2647 |
This theorem is referenced by: eupicka 2712 2eu8 2739 nfreu1 3368 eusv2i 5285 eusv2nf 5286 reusv2lem3 5291 iota2 6337 sniota 6339 fv3 6681 tz6.12c 6688 eusvobj1 7139 opiota 7746 dfac5lem5 9541 bnj1366 32000 bnj849 32096 pm14.24 40641 eu2ndop1stv 43201 tz6.12c-afv2 43318 setrec2lem2 44725 |
Copyright terms: Public domain | W3C validator |