Theorem reu5 3349

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 2566	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3348	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3058	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3347	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 628	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃*wmo 2535  ∃!weu 2565  ∃wrex 3057  ∃!wreu 3345  ∃*wrmo 3346

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 207  df-an 396  df-eu 2566  df-rex 3058  df-rmo 3347  df-reu 3348

This theorem is referenced by:  reurmo  3350  reurex  3351  cbvreuw  3373  reueq1  3379  reueq1f  3387  reu4  3686  reueq  3692  2reu5a  3699  2reurex  3715  2rexreu  3717  reuan  3843  2reu1  3844  reusv1  5337  wereu  5615  wereu2  5616  fncnv  6559  moriotass  7341  supeu  9345  infeu  9389  ttrcltr  9613  resqreu  15161  sqrtneg  15176  sqreu  15270  catideu  17583  poslubd  18319  ismgmid  18575  mndideu  18655  frlmup4  21740  evlseu  22019  ply1divalg  26071  2sqreulem1  27385  2sqreunnlem1  27388  nosupno  27643  nosupbday  27645  nosupbnd1  27654  nosupbnd2  27656  noinfno  27658  noinfbday  27660  noinfbnd1  27669  noinfbnd2  27671  noreceuw  28131  tglinethrueu  28618  foot  28701  mideu  28717  nbusgredgeu  29346  pjhtheu  31376  pjpreeq  31380  cnlnadjeui  32059  cvmliftlem14  35362  cvmlift2lem13  35380  cvmlift3  35393  r1peuqusdeg1  35708  linethrueu  36221  phpreu  37664  poimirlem18  37698  poimirlem21  37701  primrootsunit1  42210  addinvcom  42550  reutruALT  48929  lubeldm2  49080  glbeldm2  49081  upeu  49296