| 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 2589. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
| Ref | Expression |
|---|---|
| nfeu1 | ⊢ Ⅎ𝑥∃!𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eu6 2574 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | |
| 2 | nfa1 2151 | . . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦) | |
| 3 | 2 | nfex 2324 | . 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) |
| 4 | 1, 3 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥∃!𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∀wal 1538 ∃wex 1779 Ⅎwnf 1783 ∃!weu 2568 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-10 2141 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-mo 2540 df-eu 2569 |
| This theorem is referenced by: eupicka 2634 2eu8 2659 nfreu1 3412 eusv2i 5394 eusv2nf 5395 reusv2lem3 5400 iota2 6550 sniota 6552 fv3 6924 tz6.12cOLD 6933 eusvobj1 7424 opiota 8084 dfac5lem5 10167 bnj1366 34843 bnj849 34939 pm14.24 44451 eu2ndop1stv 47137 tz6.12c-afv2 47254 setrec2lem2 49213 |
| Copyright terms: Public domain | W3C validator |