Theorem reu5 3390

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 2572	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3389	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3077	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3388	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 627	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 303	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃*wmo 2541  ∃!weu 2571  ∃wrex 3076  ∃!wreu 3386  ∃*wrmo 3387

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 2572  df-rex 3077  df-rmo 3388  df-reu 3389

This theorem is referenced by:  reurmo  3391  reurex  3392  cbvreuw  3418  reueq1  3426  reueq1f  3432  reu4  3753  reueq  3759  2reu5a  3766  2reurex  3782  2rexreu  3784  reuan  3918  2reu1  3919  reusv1  5415  wereu  5696  wereu2  5697  fncnv  6651  moriotass  7437  supeu  9523  infeu  9565  ttrcltr  9785  resqreu  15301  sqrtneg  15316  sqreu  15409  catideu  17733  poslubd  18483  ismgmid  18703  mndideu  18783  frlmup4  21844  evlseu  22130  ply1divalg  26197  2sqreulem1  27508  2sqreunnlem1  27511  nosupno  27766  nosupbday  27768  nosupbnd1  27777  nosupbnd2  27779  noinfno  27781  noinfbday  27783  noinfbnd1  27792  noinfbnd2  27794  noreceuw  28235  tglinethrueu  28665  foot  28748  mideu  28764  nbusgredgeu  29401  pjhtheu  31426  pjpreeq  31430  cnlnadjeui  32109  cvmliftlem14  35265  cvmlift2lem13  35283  cvmlift3  35296  r1peuqusdeg1  35611  linethrueu  36120  phpreu  37564  poimirlem18  37598  poimirlem21  37601  primrootsunit1  42054  addinvcom  42407  reutruALT  48538  lubeldm2  48636  glbeldm2  48637