Theorem reu5 3430

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 2654	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3145	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3144	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3146	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 628	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 305	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃*wmo 2620  ∃!weu 2653  ∃wrex 3139  ∃!wreu 3140  ∃*wrmo 3141

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 209  df-an 399  df-eu 2654  df-rex 3144  df-reu 3145  df-rmo 3146

This theorem is referenced by:  reurex  3431  reurmo  3433  reu4  3722  reueq  3728  2reu5a  3735  2reurex  3750  2rexreu  3753  reuan  3880  2reu1  3881  reusv1  5298  wereu  5551  wereu2  5552  fncnv  6427  moriotass  7146  supeu  8918  infeu  8960  resqreu  14612  sqrtneg  14627  sqreu  14720  catideu  16946  poslubd  17758  ismgmid  17875  mndideu  17922  evlseu  20296  frlmup4  20945  ply1divalg  24731  2sqreulem1  26022  2sqreunnlem1  26025  tglinethrueu  26425  foot  26508  mideu  26524  nbusgredgeu  27148  pjhtheu  29171  pjpreeq  29175  cnlnadjeui  29854  cvmliftlem14  32544  cvmlift2lem13  32562  cvmlift3  32575  nosupno  33203  nosupbday  33205  nosupbnd1  33214  nosupbnd2  33216  linethrueu  33617  phpreu  34891  poimirlem18  34925  poimirlem21  34928