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  3728  reueq  3734  2reu5a  3741  2reurex  3757  2rexreu  3759  reuan  3891  2reu1  3892  reusv1  5396  wereu  5673  wereu2  5674  fncnv  6622  moriotass  7398  supeu  9449  infeu  9491  ttrcltr  9711  resqreu  15199  sqrtneg  15214  sqreu  15307  catideu  17619  poslubd  18366  ismgmid  18584  mndideu  18636  frlmup4  21356  evlseu  21646  ply1divalg  25655  2sqreulem1  26949  2sqreunnlem1  26952  nosupno  27206  nosupbday  27208  nosupbnd1  27217  nosupbnd2  27219  noinfno  27221  noinfbday  27223  noinfbnd1  27232  noinfbnd2  27234  noreceuw  27639  tglinethrueu  27890  foot  27973  mideu  27989  nbusgredgeu  28623  pjhtheu  30647  pjpreeq  30651  cnlnadjeui  31330  cvmliftlem14  34288  cvmlift2lem13  34306  cvmlift3  34319  linethrueu  35128  phpreu  36472  poimirlem18  36506  poimirlem21  36509  addinvcom  41304  reutruALT  47491  lubeldm2  47589  glbeldm2  47590