Theorem reu4 3753

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3067  ∃wrex 3076  ∃!wreu 3386  ∃*wrmo 3387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-eu 2572  df-clel 2819  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389

This theorem is referenced by:  reuind  3775  oawordeulem  8610  fin23lem23  10395  nqereu  10998  receu  11935  lbreu  12245  cju  12289  fprodser  15997  divalglem9  16449  ndvdssub  16457  qredeu  16705  pj1eu  19738  efgredeu  19794  lspsneu  21148  qtopeu  23745  qtophmeo  23846  minveclem7  25488  ig1peu  26234  coeeu  26284  plydivalg  26359  nocvxmin  27841  hlcgreu  28644  mirreu3  28680  trgcopyeu  28832  axcontlem2  28998  umgr2edg1  29246  umgr2edgneu  29249  usgredgreu  29253  uspgredg2vtxeu  29255  4cycl2vnunb  30322  frgr2wwlk1  30361  minvecolem7  30915  hlimreui  31271  riesz4i  32095  cdjreui  32464  xreceu  32886  cvmseu  35244  segconeu  35975  outsideofeu  36095  poimirlem4  37584  bfp  37784  exidu1  37816  rngoideu  37863  lshpsmreu  39065  cdleme  40517  lcfl7N  41458  mapdpg  41663  hdmap14lem6  41830  mpaaeu  43107  icceuelpart  47310  isuspgrim0lem  47755