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 3371

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 2597	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3370	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3090	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3369	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 639	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 306	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 209 ∧ wa 400 ∃wex 1809 ∈ wcel 2143 ∃*wmo 2565 ∃!weu 2596 ∃wrex 3089 ∃!wreu 3367 ∃*wrmo 3368

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 210 df-an 401 df-eu 2597 df-rex 3090 df-rmo 3369 df-reu 3370

This theorem is referenced by: reurmo 3372 reurex 3373 cbvreuw 3395 reueq1 3401 reueq1f 3407 reu4 3694 reueq 3700 2reu5a 3707 2reurex 3723 2rexreu 3725 reuan 3850 2reu1 3851 reusv1 5368 wereu 5657 wereu2 5658 fncnv 6609 moriotass 7399 supeu 9410 infeu 9454 ttrcltr 9681 resqreu 15299 sqrtneg 15314 sqreu 15408 catideu 17726 poslubd 18462 ismgmid 18718 mndideu 18798 frlmup4 21951 evlseu 22234 ply1divalg 26295 2sqreulem1 27610 2sqreunnlem1 27613 nosupno 27867 nosupbday 27869 nosupbnd1 27878 nosupbnd2 27880 noinfno 27882 noinfbday 27884 noinfbnd1 27893 noinfbnd2 27895 noreceuw 28384 tglinethrueu 28912 foot 29002 mideu 29019 prlngeu 29205 nbusgredgeu 29716 pjhtheu 31746 pjpreeq 31750 cnlnadjeui 32429 cvmliftlem14 35789 cvmlift2lem13 35807 cvmlift3 35820 r1peuqusdeg1 36135 linethrueu 36648 phpreu 38255 poimirlem18 38289 poimirlem21 38292 raldmqsmo 39012 disjimdmqseq 39458 primrootsunit1 42864 addinvcom 43193 reutruALT 49583 lubeldm2 49734 glbeldm2 49735 upeu 49949 ralsanmo 50589