![]() |
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 2587. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu6 2572 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
2 | nfa1 2149 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
3 | 2 | nfex 2323 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
4 | 1, 3 | nfxfr 1850 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∀wal 1535 ∃wex 1776 Ⅎwnf 1780 ∃!weu 2566 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-10 2139 ax-11 2155 ax-12 2175 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 df-mo 2538 df-eu 2567 |
This theorem is referenced by: eupicka 2632 2eu8 2657 nfreu1 3410 eusv2i 5400 eusv2nf 5401 reusv2lem3 5406 iota2 6552 sniota 6554 fv3 6925 tz6.12cOLD 6934 eusvobj1 7424 opiota 8083 dfac5lem5 10165 bnj1366 34822 bnj849 34918 pm14.24 44428 eu2ndop1stv 47075 tz6.12c-afv2 47192 setrec2lem2 48925 |
Copyright terms: Public domain | W3C validator |