Theorem reu4 3722

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)

Hypothesis

Ref	Expression
rmo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
reu4	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu4

Step	Hyp	Ref	Expression
1		reu5 3430	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3721	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 624	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 277	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wral 3138  ∃wrex 3139  ∃!wreu 3140  ∃*wrmo 3141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654  df-clel 2893  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146

This theorem is referenced by:  reuind  3744  oawordeulem  8180  fin23lem23  9748  nqereu  10351  receu  11285  lbreu  11591  cju  11634  fprodser  15303  divalglem9  15752  ndvdssub  15760  qredeu  16002  pj1eu  18822  efgredeu  18878  lspsneu  19895  qtopeu  22324  qtophmeo  22425  minveclem7  24038  ig1peu  24765  coeeu  24815  plydivalg  24888  hlcgreu  26404  mirreu3  26440  trgcopyeu  26592  axcontlem2  26751  umgr2edg1  26993  umgr2edgneu  26996  usgredgreu  27000  uspgredg2vtxeu  27002  4cycl2vnunb  28069  frgr2wwlk1  28108  minvecolem7  28660  hlimreui  29016  riesz4i  29840  cdjreui  30209  xreceu  30598  cvmseu  32523  nocvxmin  33248  segconeu  33472  outsideofeu  33592  poimirlem4  34911  bfp  35117  exidu1  35149  rngoideu  35196  lshpsmreu  36260  cdleme  37711  lcfl7N  38652  mapdpg  38857  hdmap14lem6  39024  mpaaeu  39770  icceuelpart  43616