Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > reu5 | GIF version |
Description: Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
Ref | Expression |
---|---|
reu5 | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eu5 2060 | . 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
2 | df-reu 2449 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | df-rex 2448 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rmo 2450 | . . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 3, 4 | anbi12i 456 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
6 | 1, 2, 5 | 3bitr4i 211 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wex 1479 ∃!weu 2013 ∃*wmo 2014 ∈ wcel 2135 ∃wrex 2443 ∃!wreu 2444 ∃*wrmo 2445 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-rex 2448 df-reu 2449 df-rmo 2450 |
This theorem is referenced by: reurex 2677 reurmo 2678 reu4 2915 reueq 2920 reusv1 4430 fncnv 5248 moriotass 5820 supeuti 6950 infeuti 6985 lteupri 7549 elrealeu 7761 rereceu 7821 exbtwnz 10176 rersqreu 10956 divalglemeunn 11843 divalglemeuneg 11845 bezoutlemeu 11925 pw2dvdseu 12079 dedekindeu 13148 dedekindicclemicc 13157 |
Copyright terms: Public domain | W3C validator |