Theorem reu5 3433

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1779   ∈ wcel 2113  ∃*wmo 2619  ∃!weu 2652  ∃wrex 3142  ∃!wreu 3143  ∃*wrmo 3144

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 2653  df-rex 3147  df-reu 3148  df-rmo 3149

This theorem is referenced by:  reurex  3434  reurmo  3436  reu4  3725  reueq  3731  2reu5a  3738  2reurex  3753  2rexreu  3756  reuan  3883  2reu1  3884  reusv1  5301  wereu  5554  wereu2  5555  fncnv  6430  moriotass  7149  supeu  8921  infeu  8963  resqreu  14615  sqrtneg  14630  sqreu  14723  catideu  16949  poslubd  17761  ismgmid  17878  mndideu  17925  evlseu  20299  frlmup4  20948  ply1divalg  24734  2sqreulem1  26025  2sqreunnlem1  26028  tglinethrueu  26428  foot  26511  mideu  26527  nbusgredgeu  27151  pjhtheu  29174  pjpreeq  29178  cnlnadjeui  29857  cvmliftlem14  32548  cvmlift2lem13  32566  cvmlift3  32579  nosupno  33207  nosupbday  33209  nosupbnd1  33218  nosupbnd2  33220  linethrueu  33621  phpreu  34880  poimirlem18  34914  poimirlem21  34917