Theorem reu5 3352

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃*wmo 2537  ∃!weu 2568  ∃wrex 3060  ∃!wreu 3348  ∃*wrmo 3349

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 2569  df-rex 3061  df-rmo 3350  df-reu 3351

This theorem is referenced by:  reurmo  3353  reurex  3354  cbvreuw  3376  reueq1  3382  reueq1f  3390  reu4  3689  reueq  3695  2reu5a  3702  2reurex  3718  2rexreu  3720  reuan  3846  2reu1  3847  reusv1  5342  wereu  5620  wereu2  5621  fncnv  6565  moriotass  7347  supeu  9357  infeu  9401  ttrcltr  9625  resqreu  15175  sqrtneg  15190  sqreu  15284  catideu  17598  poslubd  18334  ismgmid  18590  mndideu  18670  frlmup4  21756  evlseu  22038  ply1divalg  26099  2sqreulem1  27413  2sqreunnlem1  27416  nosupno  27671  nosupbday  27673  nosupbnd1  27682  nosupbnd2  27684  noinfno  27686  noinfbday  27688  noinfbnd1  27697  noinfbnd2  27699  noreceuw  28187  tglinethrueu  28711  foot  28794  mideu  28810  nbusgredgeu  29439  pjhtheu  31469  pjpreeq  31473  cnlnadjeui  32152  cvmliftlem14  35491  cvmlift2lem13  35509  cvmlift3  35522  r1peuqusdeg1  35837  linethrueu  36350  phpreu  37805  poimirlem18  37839  poimirlem21  37842  primrootsunit1  42351  addinvcom  42687  reutruALT  49050  lubeldm2  49201  glbeldm2  49202  upeu  49416