Theorem reu4 3689

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3051  ∃wrex 3060  ∃!wreu 3348  ∃*wrmo 3349

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 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569  df-clel 2811  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351

This theorem is referenced by:  reuind  3711  oawordeulem  8481  fin23lem23  10236  nqereu  10840  receu  11782  lbreu  12092  cju  12141  fprodser  15872  divalglem9  16328  ndvdssub  16336  qredeu  16585  pj1eu  19625  efgredeu  19681  lspsneu  21078  qtopeu  23660  qtophmeo  23761  minveclem7  25391  ig1peu  26136  coeeu  26186  plydivalg  26263  nocvxmin  27751  hlcgreu  28690  mirreu3  28726  trgcopyeu  28878  axcontlem2  29038  umgr2edg1  29284  umgr2edgneu  29287  usgredgreu  29291  uspgredg2vtxeu  29293  4cycl2vnunb  30365  frgr2wwlk1  30404  minvecolem7  30958  hlimreui  31314  riesz4i  32138  cdjreui  32507  xreceu  33003  cvmseu  35470  segconeu  36205  outsideofeu  36325  poimirlem4  37825  bfp  38025  exidu1  38057  rngoideu  38104  lshpsmreu  39379  cdleme  40830  lcfl7N  41771  mapdpg  41976  hdmap14lem6  42143  rediveud  42708  mpaaeu  43402  icceuelpart  47692  isuspgrim0lem  48149