Theorem reu5 3379

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

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃*wmo 2533  ∃!weu 2563  ∃wrex 3071  ∃!wreu 3375  ∃*wrmo 3376

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 206  df-an 398  df-eu 2564  df-rex 3072  df-rmo 3377  df-reu 3378

This theorem is referenced by:  reurmo  3380  reurex  3381  cbvreuw  3407  reueq1  3416  reueq1f  3422  reu4  3727  reueq  3733  2reu5a  3740  2reurex  3756  2rexreu  3758  reuan  3890  2reu1  3891  reusv1  5395  wereu  5672  wereu2  5673  fncnv  6619  moriotass  7395  supeu  9446  infeu  9488  ttrcltr  9708  resqreu  15196  sqrtneg  15211  sqreu  15304  catideu  17616  poslubd  18363  ismgmid  18581  mndideu  18633  frlmup4  21348  evlseu  21638  ply1divalg  25647  2sqreulem1  26939  2sqreunnlem1  26942  nosupno  27196  nosupbday  27198  nosupbnd1  27207  nosupbnd2  27209  noinfno  27211  noinfbday  27213  noinfbnd1  27222  noinfbnd2  27224  noreceuw  27629  tglinethrueu  27880  foot  27963  mideu  27979  nbusgredgeu  28613  pjhtheu  30635  pjpreeq  30639  cnlnadjeui  31318  cvmliftlem14  34277  cvmlift2lem13  34295  cvmlift3  34308  linethrueu  35117  phpreu  36461  poimirlem18  36495  poimirlem21  36498  addinvcom  41301  reutruALT  47445  lubeldm2  47543  glbeldm2  47544