Theorem reu5 3136

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		eu5 2484	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 2903	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 2902	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 2904	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 729	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 291	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  ∃*wmo 2459  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463  df-rex 2902  df-reu 2903  df-rmo 2904

This theorem is referenced by:  reurex  3137  reurmo  3138  reu4  3367  reueq  3371  reusv1  4792  reusv1OLD  4793  wereu  5034  wereu2  5035  fncnv  5876  moriotass  6539  supeu  8243  infeu  8285  resqreu  13841  sqrtneg  13856  sqreu  13948  catideu  16159  poslubd  16971  ismgmid  17087  mndideu  17127  evlseu  19337  frlmup4  19959  ply1divalg  23701  tglinethrueu  25334  foot  25414  mideu  25430  pjhtheu  27637  pjpreeq  27641  cnlnadjeui  28320  cvmliftlem14  30533  cvmlift2lem13  30551  cvmlift3  30564  linethrueu  31433  phpreu  32563  poimirlem18  32597  poimirlem21  32600  2reu5a  39826  reuan  39829  2reurex  39830  2rexreu  39834  2reu1  39835  nbusgredgeu  40594