Theorem reu5 3358

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃*wmo 2532  ∃!weu 2562  ∃wrex 3054  ∃!wreu 3354  ∃*wrmo 3355

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 2563  df-rex 3055  df-rmo 3356  df-reu 3357

This theorem is referenced by:  reurmo  3359  reurex  3360  cbvreuw  3384  reueq1  3391  reueq1f  3399  reu4  3705  reueq  3711  2reu5a  3718  2reurex  3734  2rexreu  3736  reuan  3862  2reu1  3863  reusv1  5355  wereu  5637  wereu2  5638  fncnv  6592  moriotass  7379  supeu  9412  infeu  9456  ttrcltr  9676  resqreu  15225  sqrtneg  15240  sqreu  15334  catideu  17643  poslubd  18379  ismgmid  18599  mndideu  18679  frlmup4  21717  evlseu  21997  ply1divalg  26050  2sqreulem1  27364  2sqreunnlem1  27367  nosupno  27622  nosupbday  27624  nosupbnd1  27633  nosupbnd2  27635  noinfno  27637  noinfbday  27639  noinfbnd1  27648  noinfbnd2  27650  noreceuw  28101  tglinethrueu  28573  foot  28656  mideu  28672  nbusgredgeu  29300  pjhtheu  31330  pjpreeq  31334  cnlnadjeui  32013  cvmliftlem14  35291  cvmlift2lem13  35309  cvmlift3  35322  r1peuqusdeg1  35637  linethrueu  36151  phpreu  37605  poimirlem18  37639  poimirlem21  37642  primrootsunit1  42092  addinvcom  42427  reutruALT  48797  lubeldm2  48948  glbeldm2  48949  upeu  49164