Theorem reu5 3354

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 2586	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
2		df-reu 3096	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3		df-rex 3095	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rmo 3097	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	anbi12i 620	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
6	1, 2, 5	3bitr4i 295	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))

Syntax hints:   ↔ wb 198   ∧ wa 386  ∃wex 1823   ∈ wcel 2106  ∃*wmo 2548  ∃!weu 2585  ∃wrex 3090  ∃!wreu 3091  ∃*wrmo 3092

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 199  df-an 387  df-eu 2586  df-rex 3095  df-reu 3096  df-rmo 3097

This theorem is referenced by:  reurex  3355  reurmo  3356  reu4  3611  reueq  3617  reusv1  5109  wereu  5351  wereu2  5352  fncnv  6207  moriotass  6912  supeu  8648  infeu  8690  resqreu  14400  sqrtneg  14415  sqreu  14507  catideu  16721  poslubd  17534  ismgmid  17650  mndideu  17690  evlseu  19912  frlmup4  20544  ply1divalg  24334  tglinethrueu  25990  foot  26070  mideu  26086  nbusgredgeu  26713  pjhtheu  28825  pjpreeq  28829  cnlnadjeui  29508  cvmliftlem14  31878  cvmlift2lem13  31896  cvmlift3  31909  nosupno  32438  nosupbday  32440  nosupbnd1  32449  nosupbnd2  32451  linethrueu  32852  phpreu  34002  poimirlem18  34037  poimirlem21  34040  2reu5a  42117  reuan  42120  2reurex  42124  2rexreu  42128  2reu1  42129