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 2444 | . 2 wff ∃!𝑥 ∈ 𝐴 𝜑 |
5 | 2 | cv 1341 | . . . . 5 class 𝑥 |
6 | 5, 3 | wcel 2135 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 6, 1 | wa 103 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝜑) |
8 | 7, 2 | weu 2013 | . 2 wff ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) |
9 | 4, 8 | wb 104 | 1 wff (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: nfreu1 2635 nfreudxy 2637 reubida 2645 reubiia 2648 reueq1f 2657 reu5 2676 rmo5 2679 cbvreu 2687 cbvreuvw 2695 reuv 2740 reu2 2909 reu6 2910 reu3 2911 2reuswapdc 2925 cbvreucsf 3104 reuss2 3397 reuun2 3400 reupick 3401 reupick3 3402 reusn 3641 rabsneu 3643 reuhypd 4443 funcnv3 5244 feu 5364 dff4im 5625 f1ompt 5630 fsn 5651 riotauni 5798 riotacl2 5805 riota1 5810 riota1a 5811 riota2df 5812 snriota 5821 riotaund 5826 acexmid 5835 climreu 11224 divalgb 11847 uptx 12821 txcn 12822 dedekindicc 13158 bdcriota 13606 |
Copyright terms: Public domain | W3C validator |