Theorem reu4 3670

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 3375	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3669	. . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
4	3	anbi2i 625	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))
5	1, 4	bitri 278	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wral 3106  ∃wrex 3107  ∃!wreu 3108  ∃*wrmo 3109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629  df-clel 2870  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114

This theorem is referenced by:  reuind  3692  oawordeulem  8163  fin23lem23  9737  nqereu  10340  receu  11274  lbreu  11578  cju  11621  fprodser  15295  divalglem9  15742  ndvdssub  15750  qredeu  15992  pj1eu  18814  efgredeu  18870  lspsneu  19888  qtopeu  22321  qtophmeo  22422  minveclem7  24039  ig1peu  24772  coeeu  24822  plydivalg  24895  hlcgreu  26412  mirreu3  26448  trgcopyeu  26600  axcontlem2  26759  umgr2edg1  27001  umgr2edgneu  27004  usgredgreu  27008  uspgredg2vtxeu  27010  4cycl2vnunb  28075  frgr2wwlk1  28114  minvecolem7  28666  hlimreui  29022  riesz4i  29846  cdjreui  30215  xreceu  30624  cvmseu  32636  nocvxmin  33361  segconeu  33585  outsideofeu  33705  poimirlem4  35061  bfp  35262  exidu1  35294  rngoideu  35341  lshpsmreu  36405  cdleme  37856  lcfl7N  38797  mapdpg  39002  hdmap14lem6  39169  mpaaeu  40094  icceuelpart  43953