| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > reu5 | Structured version Visualization version 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 | df-eu 2569 | . 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) | |
| 2 | df-reu 3381 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 3 | df-rex 3071 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 4 | df-rmo 3380 | . . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 5 | 3, 4 | anbi12i 628 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))) |
| 6 | 1, 2, 5 | 3bitr4i 303 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃*wmo 2538 ∃!weu 2568 ∃wrex 3070 ∃!wreu 3378 ∃*wrmo 3379 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-eu 2569 df-rex 3071 df-rmo 3380 df-reu 3381 |
| This theorem is referenced by: reurmo 3383 reurex 3384 cbvreuw 3410 reueq1 3417 reueq1f 3425 reu4 3737 reueq 3743 2reu5a 3750 2reurex 3766 2rexreu 3768 reuan 3896 2reu1 3897 reusv1 5397 wereu 5681 wereu2 5682 fncnv 6639 moriotass 7420 supeu 9494 infeu 9536 ttrcltr 9756 resqreu 15291 sqrtneg 15306 sqreu 15399 catideu 17718 poslubd 18458 ismgmid 18678 mndideu 18758 frlmup4 21821 evlseu 22107 ply1divalg 26177 2sqreulem1 27490 2sqreunnlem1 27493 nosupno 27748 nosupbday 27750 nosupbnd1 27759 nosupbnd2 27761 noinfno 27763 noinfbday 27765 noinfbnd1 27774 noinfbnd2 27776 noreceuw 28217 tglinethrueu 28647 foot 28730 mideu 28746 nbusgredgeu 29383 pjhtheu 31413 pjpreeq 31417 cnlnadjeui 32096 cvmliftlem14 35302 cvmlift2lem13 35320 cvmlift3 35333 r1peuqusdeg1 35648 linethrueu 36157 phpreu 37611 poimirlem18 37645 poimirlem21 37648 primrootsunit1 42098 addinvcom 42461 reutruALT 48725 lubeldm2 48853 glbeldm2 48854 upeu 48928 |
| Copyright terms: Public domain | W3C validator |