Theorem reu4 3672

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wral 3053  ∃wrex 3063  ∃!wreu 3342  ∃*wrmo 3343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-eu 2573  df-clel 2814  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345

This theorem is referenced by:  reuind  3694  oawordeulem  8479  fin23lem23  10239  nqereu  10843  receu  11786  lbreu  12097  cju  12146  fprodser  15905  divalglem9  16361  ndvdssub  16369  qredeu  16618  pj1eu  19662  efgredeu  19718  lspsneu  21116  qtopeu  23699  qtophmeo  23800  minveclem7  25420  ig1peu  26158  coeeu  26208  plydivalg  26283  nocvxmin  27765  hlcgreu  28704  mirreu3  28740  trgcopyeu  28892  axcontlem2  29052  umgr2edg1  29298  umgr2edgneu  29301  usgredgreu  29305  uspgredg2vtxeu  29307  4cycl2vnunb  30378  frgr2wwlk1  30417  minvecolem7  30972  hlimreui  31328  riesz4i  32152  cdjreui  32521  xreceu  33000  cvmseu  35504  segconeu  36239  outsideofeu  36359  poimirlem4  37991  bfp  38191  exidu1  38223  rngoideu  38270  lshpsmreu  39601  cdleme  41052  lcfl7N  41993  mapdpg  42198  hdmap14lem6  42365  rediveud  42920  mpaaeu  43595  icceuelpart  47911  isuspgrim0lem  48384