Theorem reu5 3353

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 2562	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3352	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3351	. . 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 2531  ∃!weu 2561  ∃wrex 3053  ∃!wreu 3349  ∃*wrmo 3350

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 2562  df-rex 3054  df-rmo 3351  df-reu 3352

This theorem is referenced by:  reurmo  3354  reurex  3355  cbvreuw  3379  reueq1  3385  reueq1f  3393  reu4  3699  reueq  3705  2reu5a  3712  2reurex  3728  2rexreu  3730  reuan  3856  2reu1  3857  reusv1  5347  wereu  5627  wereu2  5628  fncnv  6573  moriotass  7358  supeu  9381  infeu  9425  ttrcltr  9645  resqreu  15194  sqrtneg  15209  sqreu  15303  catideu  17616  poslubd  18352  ismgmid  18574  mndideu  18654  frlmup4  21743  evlseu  22023  ply1divalg  26076  2sqreulem1  27390  2sqreunnlem1  27393  nosupno  27648  nosupbday  27650  nosupbnd1  27659  nosupbnd2  27661  noinfno  27663  noinfbday  27665  noinfbnd1  27674  noinfbnd2  27676  noreceuw  28134  tglinethrueu  28619  foot  28702  mideu  28718  nbusgredgeu  29346  pjhtheu  31373  pjpreeq  31377  cnlnadjeui  32056  cvmliftlem14  35277  cvmlift2lem13  35295  cvmlift3  35308  r1peuqusdeg1  35623  linethrueu  36137  phpreu  37591  poimirlem18  37625  poimirlem21  37628  primrootsunit1  42078  addinvcom  42413  reutruALT  48786  lubeldm2  48937  glbeldm2  48938  upeu  49153