Theorem reu4 3685

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3047  ∃wrex 3056  ∃!wreu 3344  ∃*wrmo 3345

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 1968  ax-7 2009  ax-8 2113

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2535  df-eu 2564  df-clel 2806  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347

This theorem is referenced by:  reuind  3707  oawordeulem  8469  fin23lem23  10217  nqereu  10820  receu  11762  lbreu  12072  cju  12121  fprodser  15856  divalglem9  16312  ndvdssub  16320  qredeu  16569  pj1eu  19608  efgredeu  19664  lspsneu  21060  qtopeu  23631  qtophmeo  23732  minveclem7  25362  ig1peu  26107  coeeu  26157  plydivalg  26234  nocvxmin  27718  hlcgreu  28596  mirreu3  28632  trgcopyeu  28784  axcontlem2  28943  umgr2edg1  29189  umgr2edgneu  29192  usgredgreu  29196  uspgredg2vtxeu  29198  4cycl2vnunb  30270  frgr2wwlk1  30309  minvecolem7  30863  hlimreui  31219  riesz4i  32043  cdjreui  32412  xreceu  32902  cvmseu  35320  segconeu  36055  outsideofeu  36175  poimirlem4  37674  bfp  37874  exidu1  37906  rngoideu  37953  lshpsmreu  39218  cdleme  40669  lcfl7N  41610  mapdpg  41815  hdmap14lem6  41982  rediveud  42546  mpaaeu  43253  icceuelpart  47546  isuspgrim0lem  48003