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 3373

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 2599	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3372	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3092	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3371	. . 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 2146 ∃*wmo 2567 ∃!weu 2598 ∃wrex 3091 ∃!wreu 3369 ∃*wrmo 3370

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 2599 df-rex 3092 df-rmo 3371 df-reu 3372

This theorem is used by: reurmo 3374 reurex 3375 cbvreuw 3397 reueq1 3403 reueq1f 3409 reu4 3696 reueq 3702 2reu5a 3709 2reurex 3725 2rexreu 3727 reuan 3851 2reu1 3852 reusv1 5370 wereu 5659 wereu2 5660 fncnv 6613 moriotass 7408 supeu 9421 infeu 9465 ttrcltr 9692 resqreu 15327 sqrtneg 15342 sqreu 15436 catideu 17753 poslubd 18489 mgmideud 18743 ismgmid 18748 mndideuOLD 18836 frlmup4 22001 evlseu 22284 ply1divalg 26346 2sqreulem1 27661 2sqreunnlem1 27664 nosupno 27918 nosupbday 27920 nosupbnd1 27929 nosupbnd2 27931 noinfno 27933 noinfbday 27935 noinfbnd1 27944 noinfbnd2 27946 noreceuw 28435 tglinethrueu 28963 foot 29053 mideu 29070 prlngeu 29260 nbusgredgeu 29774 pjhtheu 31817 pjpreeq 31821 cnlnadjeui 32500 cvmliftlem14 35826 cvmlift2lem13 35844 cvmlift3 35857 r1peuqusdeg1 36172 linethrueu 36685 phpreu 38312 poimirlem18 38346 poimirlem21 38349 raldmqsmo 39070 disjimdmqseq 39516 primrootsunit1 42922 addinvcom 43251 reutruALT 49640 lubeldm2 49791 glbeldm2 49792 upeu 50006 ralsanmo 50646