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 1812 ∈ wcel 2145 ∃*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 3689 reueq 3695 2reu5a 3702 2reurex 3718 2rexreu 3720 reuan 3844 2reu1 3845 reusv1 5362 wereu 5651 wereu2 5652 fncnv 6606 moriotass 7402 supeu 9424 infeu 9468 ttrcltr 9695 resqreu 15339 sqrtneg 15354 sqreu 15448 catideu 17763 poslubd 18499 mgmideud 18753 ismgmid 18758 mndideuOLD 18848 frlmup4 22014 evlseu 22299 ply1divalg 26363 2sqreulem1 27682 2sqreunnlem1 27685 nosupno 27939 nosupbday 27941 nosupbnd1 27950 nosupbnd2 27952 noinfno 27954 noinfbday 27956 noinfbnd1 27965 noinfbnd2 27967 noreceuw 28456 tglinethrueu 28986 foot 29076 mideu 29093 prlngeu 29312 nbusgredgeu 29826 pjhtheu 31875 pjpreeq 31879 cnlnadjeui 32558 cvmliftlem14 35876 cvmlift2lem13 35894 cvmlift3 35907 r1peuqusdeg1 36222 linethrueu 36736 phpreu 38358 poimirlem18 38387 poimirlem21 38390 raldmqsmo 39111 disjimdmqseq 39557 primrootsunit1 42963 addinvcom 43307 reutruALT 49733 lubeldm2 49882 glbeldm2 49883 upeu 50097 ralsanmo 50740