Theorem reu4 3727

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wral 3061  ∃wrex 3070  ∃!wreu 3374  ∃*wrmo 3375

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534  df-eu 2563  df-clel 2810  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377

This theorem is referenced by:  reuind  3749  oawordeulem  8556  fin23lem23  10323  nqereu  10926  receu  11861  lbreu  12166  cju  12210  fprodser  15895  divalglem9  16346  ndvdssub  16354  qredeu  16597  pj1eu  19566  efgredeu  19622  lspsneu  20742  qtopeu  23227  qtophmeo  23328  minveclem7  24959  ig1peu  25696  coeeu  25746  plydivalg  25819  nocvxmin  27287  hlcgreu  27907  mirreu3  27943  trgcopyeu  28095  axcontlem2  28261  umgr2edg1  28506  umgr2edgneu  28509  usgredgreu  28513  uspgredg2vtxeu  28515  4cycl2vnunb  29581  frgr2wwlk1  29620  minvecolem7  30174  hlimreui  30530  riesz4i  31354  cdjreui  31723  xreceu  32126  cvmseu  34336  segconeu  35058  outsideofeu  35178  poimirlem4  36584  bfp  36784  exidu1  36816  rngoideu  36863  lshpsmreu  38071  cdleme  39523  lcfl7N  40464  mapdpg  40669  hdmap14lem6  40836  mpaaeu  41980  icceuelpart  46189