reu5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > reu5		Structured version Visualization version GIF version

Theorem reu5 3367

Description: Restricted uniqueness in terms of "at most one". (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.)

**Assertion**
Ref	Expression
reu5	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

**Proof of Theorem reu5**
Step	Hyp	Ref	Expression
1		df-eu 2594	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3366	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3087	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3365	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 640	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ↔ wb 209 ∧ wa 401 ∃wex 1811 ∈ wcel 2144 ∃*wmo 2562 ∃!weu 2593 ∃wrex 3086 ∃!wreu 3363 ∃*wrmo 3364

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This proof depends on definitions: df-bi 210 df-an 402 df-eu 2594 df-rex 3087 df-rmo 3365 df-reu 3366

This theorem is used by: reurmo 3368 reurex 3369 cbvreuw 3391 reueq1 3397 reueq1f 3403 reu4 3688 reueq 3694 2reu5a 3701 2reurex 3717 2rexreu 3719 reuan 3844 2reu1 3845 reusv1 5359 wereu 5647 wereu2 5648 fncnv 6618 moriotass 7413 supeu 9453 infeu 9497 ttrcltr 9724 resqreu 15428 sqrtneg 15443 sqreu 15537 catideu 17858 poslubd 18594 mgmideud 18848 ismgmid 18854 mndideuOLD 18944 frlmup4 22116 evlseu 22401 ply1divalg 26465 2sqreulem1 27782 2sqreunnlem1 27785 nosupno 28069 nosupbday 28071 nosupbnd1 28080 nosupbnd2 28082 noinfno 28084 noinfbday 28086 noinfbnd1 28095 noinfbnd2 28097 noreceuw 28586 tglinethrueu 29116 foot 29206 mideu 29223 prlngeu 29442 nbusgredgeu 29956 pjhtheu 32005 pjpreeq 32009 cnlnadjeui 32688 cvmliftlem14 36180 cvmlift2lem13 36198 cvmlift3 36211 r1peuqusdeg1 36526 linethrueu 37045 phpreu 38664 poimirlem18 38693 poimirlem21 38696 raldmqsmo 39432 disjimdmqseq 39878 primrootsunit1 43284 addinvcom 43620 reutruALT 50051 lubeldm2 50206 glbeldm2 50207 upeu 50423 ralsanmo 51118