Theorem reu5 3380

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1776   ∈ wcel 2106  ∃*wmo 2536  ∃!weu 2566  ∃wrex 3068  ∃!wreu 3376  ∃*wrmo 3377

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 2567  df-rex 3069  df-rmo 3378  df-reu 3379

This theorem is referenced by:  reurmo  3381  reurex  3382  cbvreuw  3408  reueq1  3415  reueq1f  3422  reu4  3740  reueq  3746  2reu5a  3753  2reurex  3769  2rexreu  3771  reuan  3905  2reu1  3906  reusv1  5403  wereu  5685  wereu2  5686  fncnv  6641  moriotass  7420  supeu  9492  infeu  9534  ttrcltr  9754  resqreu  15288  sqrtneg  15303  sqreu  15396  catideu  17720  poslubd  18471  ismgmid  18691  mndideu  18771  frlmup4  21839  evlseu  22125  ply1divalg  26192  2sqreulem1  27505  2sqreunnlem1  27508  nosupno  27763  nosupbday  27765  nosupbnd1  27774  nosupbnd2  27776  noinfno  27778  noinfbday  27780  noinfbnd1  27789  noinfbnd2  27791  noreceuw  28232  tglinethrueu  28662  foot  28745  mideu  28761  nbusgredgeu  29398  pjhtheu  31423  pjpreeq  31427  cnlnadjeui  32106  cvmliftlem14  35282  cvmlift2lem13  35300  cvmlift3  35313  r1peuqusdeg1  35628  linethrueu  36138  phpreu  37591  poimirlem18  37625  poimirlem21  37628  primrootsunit1  42079  addinvcom  42438  reutruALT  48654  lubeldm2  48753  glbeldm2  48754  upeu  48817