![]() |
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 | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cA | . . 3 class 𝐴 | |
4 | 1, 2, 3 | wreu 2470 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1363 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2160 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 104 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2038 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 105 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfreu1 2662 nfreudxy 2664 reubida 2672 reubiia 2675 reueq1f 2684 reu5 2703 rmo5 2706 cbvreu 2716 cbvreuvw 2724 reuv 2771 reu2 2940 reu6 2941 reu3 2942 2reuswapdc 2956 cbvreucsf 3136 reuss2 3430 reuun2 3433 reupick 3434 reupick3 3435 reusn 3678 rabsneu 3680 reuhypd 4489 funcnv3 5297 feu 5417 dff4im 5683 f1ompt 5688 fsn 5709 riotauni 5859 riotacl2 5866 riota1 5871 riota1a 5872 riota2df 5873 snriota 5882 riotaund 5887 acexmid 5896 climreu 11340 divalgb 11965 uptx 14251 txcn 14252 dedekindicc 14588 bdcriota 15113 |
Copyright terms: Public domain | W3C validator |