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 3368

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 2595	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3367	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3088	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3366	. . 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 2563 ∃!weu 2594 ∃wrex 3087 ∃!wreu 3364 ∃*wrmo 3365

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 2595 df-rex 3088 df-rmo 3366 df-reu 3367

This theorem is used by: reurmo 3369 reurex 3370 cbvreuw 3392 reueq1 3398 reueq1f 3404 reu4 3689 reueq 3695 2reu5a 3702 2reurex 3718 2rexreu 3720 reuan 3844 2reu1 3845 reusv1 5359 wereu 5647 wereu2 5648 fncnv 6613 moriotass 7409 supeu 9446 infeu 9490 ttrcltr 9717 resqreu 15419 sqrtneg 15434 sqreu 15528 catideu 17849 poslubd 18585 mgmideud 18839 ismgmid 18845 mndideuOLD 18935 frlmup4 22107 evlseu 22392 ply1divalg 26456 2sqreulem1 27773 2sqreunnlem1 27776 nosupno 28060 nosupbday 28062 nosupbnd1 28071 nosupbnd2 28073 noinfno 28075 noinfbday 28077 noinfbnd1 28086 noinfbnd2 28088 noreceuw 28577 tglinethrueu 29107 foot 29197 mideu 29214 prlngeu 29433 nbusgredgeu 29947 pjhtheu 31996 pjpreeq 32000 cnlnadjeui 32679 cvmliftlem14 36062 cvmlift2lem13 36080 cvmlift3 36093 r1peuqusdeg1 36408 linethrueu 36921 phpreu 38527 poimirlem18 38556 poimirlem21 38559 raldmqsmo 39295 disjimdmqseq 39741 primrootsunit1 43147 addinvcom 43483 reutruALT 49914 lubeldm2 50063 glbeldm2 50064 upeu 50278 ralsanmo 50906