Theorem reu5 3356

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 3355	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3054	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3354	. . 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 3352  ∃*wrmo 3353

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 3354  df-reu 3355

This theorem is referenced by:  reurmo  3357  reurex  3358  cbvreuw  3382  reueq1  3388  reueq1f  3396  reu4  3702  reueq  3708  2reu5a  3715  2reurex  3731  2rexreu  3733  reuan  3859  2reu1  3860  reusv1  5352  wereu  5634  wereu2  5635  fncnv  6589  moriotass  7376  supeu  9405  infeu  9449  ttrcltr  9669  resqreu  15218  sqrtneg  15233  sqreu  15327  catideu  17636  poslubd  18372  ismgmid  18592  mndideu  18672  frlmup4  21710  evlseu  21990  ply1divalg  26043  2sqreulem1  27357  2sqreunnlem1  27360  nosupno  27615  nosupbday  27617  nosupbnd1  27626  nosupbnd2  27628  noinfno  27630  noinfbday  27632  noinfbnd1  27641  noinfbnd2  27643  noreceuw  28094  tglinethrueu  28566  foot  28649  mideu  28665  nbusgredgeu  29293  pjhtheu  31323  pjpreeq  31327  cnlnadjeui  32006  cvmliftlem14  35284  cvmlift2lem13  35302  cvmlift3  35315  r1peuqusdeg1  35630  linethrueu  36144  phpreu  37598  poimirlem18  37632  poimirlem21  37635  primrootsunit1  42085  addinvcom  42420  reutruALT  48793  lubeldm2  48944  glbeldm2  48945  upeu  49160