New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > eu5 | GIF version |
Description: Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) |
Ref | Expression |
---|---|
eu5 | ⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1619 | . . 3 ⊢ Ⅎyφ | |
2 | 1 | eu3 2230 | . 2 ⊢ (∃!xφ ↔ (∃xφ ∧ ∃y∀x(φ → x = y))) |
3 | 1 | mo2 2233 | . . 3 ⊢ (∃*xφ ↔ ∃y∀x(φ → x = y)) |
4 | 3 | anbi2i 675 | . 2 ⊢ ((∃xφ ∧ ∃*xφ) ↔ (∃xφ ∧ ∃y∀x(φ → x = y))) |
5 | 2, 4 | bitr4i 243 | 1 ⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∃!weu 2204 ∃*wmo 2205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 |
This theorem is referenced by: eu4 2243 eumo 2244 exmoeu2 2247 euim 2254 euan 2261 2euex 2276 2euswap 2280 2exeu 2281 2eu1 2284 reu5 2824 reuss2 3535 n0moeu 3562 funeu 5131 funcnv3 5157 fnres 5199 fnopabg 5205 dff3 5420 fnce 6176 |
Copyright terms: Public domain | W3C validator |