Theorem reu5 3361

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃*wmo 2537  ∃!weu 2567  ∃wrex 3060  ∃!wreu 3357  ∃*wrmo 3358

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 2568  df-rex 3061  df-rmo 3359  df-reu 3360

This theorem is referenced by:  reurmo  3362  reurex  3363  cbvreuw  3389  reueq1  3396  reueq1f  3404  reu4  3714  reueq  3720  2reu5a  3727  2reurex  3743  2rexreu  3745  reuan  3871  2reu1  3872  reusv1  5367  wereu  5650  wereu2  5651  fncnv  6609  moriotass  7394  supeu  9466  infeu  9510  ttrcltr  9730  resqreu  15271  sqrtneg  15286  sqreu  15379  catideu  17687  poslubd  18423  ismgmid  18643  mndideu  18723  frlmup4  21761  evlseu  22041  ply1divalg  26095  2sqreulem1  27409  2sqreunnlem1  27412  nosupno  27667  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfno  27682  noinfbday  27684  noinfbnd1  27693  noinfbnd2  27695  noreceuw  28146  tglinethrueu  28618  foot  28701  mideu  28717  nbusgredgeu  29345  pjhtheu  31375  pjpreeq  31379  cnlnadjeui  32058  cvmliftlem14  35319  cvmlift2lem13  35337  cvmlift3  35350  r1peuqusdeg1  35665  linethrueu  36174  phpreu  37628  poimirlem18  37662  poimirlem21  37665  primrootsunit1  42110  addinvcom  42474  reutruALT  48784  lubeldm2  48930  glbeldm2  48931  upeu  49106