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

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1779   ∈ wcel 2104  ∃*wmo 2536  ∃!weu 2566  ∃wrex 3071  ∃!wreu 3301  ∃*wrmo 3302

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 206  df-an 398  df-eu 2567  df-rex 3072  df-rmo 3304  df-reu 3305

This theorem is referenced by:  reurex  3381  reurmo  3383  cbvreuw  3390  reu4  3671  reueq  3677  2reu5a  3684  2reurex  3700  2rexreu  3702  reuan  3834  2reu1  3835  reusv1  5329  wereu  5596  wereu2  5597  fncnv  6536  moriotass  7297  supeu  9261  infeu  9303  ttrcltr  9522  resqreu  15013  sqrtneg  15028  sqreu  15121  catideu  17433  poslubd  18180  ismgmid  18398  mndideu  18445  frlmup4  21057  evlseu  21342  ply1divalg  25351  2sqreulem1  26643  2sqreunnlem1  26646  tglinethrueu  27049  foot  27132  mideu  27148  nbusgredgeu  27782  pjhtheu  29805  pjpreeq  29809  cnlnadjeui  30488  cvmliftlem14  33308  cvmlift2lem13  33326  cvmlift3  33339  nosupno  33955  nosupbday  33957  nosupbnd1  33966  nosupbnd2  33968  noinfno  33970  noinfbday  33972  noinfbnd1  33981  noinfbnd2  33983  linethrueu  34507  phpreu  35809  poimirlem18  35843  poimirlem21  35846  addinvcom  40608  reutruALT  46396  lubeldm2  46494  glbeldm2  46495