Theorem reu4 3694

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wral 3076  ∃wrex 3086  ∃!wreu 3365  ∃*wrmo 3366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-mo 2566  df-eu 2596  df-clel 2837  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368

This theorem is referenced by:  reuind  3716  oawordeulem  8523  fin23lem23  10283  nqereu  10887  receu  11832  lbreu  12142  cju  12191  fprodser  15979  divalglem9  16435  ndvdssub  16443  qredeu  16692  pj1eu  19736  efgredeu  19792  lspsneu  21193  qtopeu  23776  qtophmeo  23877  minveclem7  25497  ig1peu  26235  coeeu  26285  plydivalg  26363  nocvxmin  27848  hlcgreu  28787  mirreu3  28827  trgcopyeu  28979  axcontlem2  29166  umgr2edg1  29412  umgr2edgneu  29415  usgredgreu  29419  uspgredg2vtxeu  29421  4cycl2vnunb  30492  frgr2wwlk1  30531  minvecolem7  31086  hlimreui  31442  riesz4i  32266  cdjreui  32635  xreceu  33099  cvmseu  35626  segconeu  36361  outsideofeu  36481  poimirlem4  38123  bfp  38323  exidu1  38355  rngoideu  38402  lshpsmreu  39733  cdleme  41184  lcfl7N  42125  mapdpg  42330  hdmap14lem6  42497  rediveud  43052  mpaaeu  43727  icceuelpart  48042  isuspgrim0lem  48515