![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-reu | GIF version |
Description: Define restricted existential uniqueness. (Contributed by NM, 22-Nov-1994.) |
Ref | Expression |
---|---|
df-reu | ⊢ (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff φ | |
2 | vx | . . 3 setvar x | |
3 | cA | . . 3 class A | |
4 | 1, 2, 3 | wreu 2302 | . 2 wff ∃!x ∈ A φ |
5 | 2 | cv 1241 | . . . . 5 class x |
6 | 5, 3 | wcel 1390 | . . . 4 wff x ∈ A |
7 | 6, 1 | wa 97 | . . 3 wff (x ∈ A ∧ φ) |
8 | 7, 2 | weu 1897 | . 2 wff ∃!x(x ∈ A ∧ φ) |
9 | 4, 8 | wb 98 | 1 wff (∃!x ∈ A φ ↔ ∃!x(x ∈ A ∧ φ)) |
Colors of variables: wff set class |
This definition is referenced by: nfreu1 2475 nfreudxy 2477 reubida 2485 reubiia 2488 reueq1f 2497 reu5 2516 rmo5 2519 cbvreu 2525 reuv 2567 reu2 2723 reu6 2724 reu3 2725 2reuswapdc 2737 cbvreucsf 2904 reuss2 3211 reuun2 3214 reupick 3215 reupick3 3216 reusn 3432 rabsneu 3434 reuhypd 4169 funcnv3 4904 feu 5015 dff4im 5256 f1ompt 5263 fsn 5278 riotauni 5417 riotacl2 5424 riota1 5429 riota1a 5430 riota2df 5431 snriota 5440 riotaund 5445 acexmid 5454 bdcriota 9338 |
Copyright terms: Public domain | W3C validator |