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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wral 3079  ∃wrex 3089  ∃!wreu 3367  ∃*wrmo 3368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-clel 2838  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370

This theorem is referenced by:  reuind  3716  oawordeulem  8535  fin23lem23  10305  nqereu  10909  receu  11854  lbreu  12160  cju  12209  fprodser  15999  divalglem9  16454  ndvdssub  16462  qredeu  16711  pj1eu  19761  efgredeu  19817  lspsneu  21247  qtopeu  23873  qtophmeo  23974  minveclem7  25594  ig1peu  26332  coeeu  26382  plydivalg  26460  nocvxmin  27948  hlcgreu  28890  mirreu3  28931  trgcopyeu  29117  axcontlem2  29315  umgr2edg1  29561  umgr2edgneu  29564  usgredgreu  29568  uspgredg2vtxeu  29570  4cycl2vnunb  30641  frgr2wwlk1  30680  minvecolem7  31235  hlimreui  31591  riesz4i  32415  cdjreui  32784  xreceu  33241  cvmseu  35768  segconeu  36503  outsideofeu  36623  poimirlem4  38295  bfp  38495  exidu1  38527  rngoideu  38574  lshpsmreu  39903  cdleme  41354  lcfl7N  42295  mapdpg  42500  hdmap14lem6  42667  rediveud  43224  mpaaeu  43897  icceuelpart  48205  isuspgrim0lem  48678