Theorem reu4 3702

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3044  ∃wrex 3053  ∃!wreu 3352  ∃*wrmo 3353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562  df-clel 2803  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355

This theorem is referenced by:  reuind  3724  oawordeulem  8518  fin23lem23  10279  nqereu  10882  receu  11823  lbreu  12133  cju  12182  fprodser  15915  divalglem9  16371  ndvdssub  16379  qredeu  16628  pj1eu  19626  efgredeu  19682  lspsneu  21033  qtopeu  23603  qtophmeo  23704  minveclem7  25335  ig1peu  26080  coeeu  26130  plydivalg  26207  nocvxmin  27690  hlcgreu  28545  mirreu3  28581  trgcopyeu  28733  axcontlem2  28892  umgr2edg1  29138  umgr2edgneu  29141  usgredgreu  29145  uspgredg2vtxeu  29147  4cycl2vnunb  30219  frgr2wwlk1  30258  minvecolem7  30812  hlimreui  31168  riesz4i  31992  cdjreui  32361  xreceu  32842  cvmseu  35263  segconeu  35999  outsideofeu  36119  poimirlem4  37618  bfp  37818  exidu1  37850  rngoideu  37897  lshpsmreu  39102  cdleme  40554  lcfl7N  41495  mapdpg  41700  hdmap14lem6  41867  rediveud  42431  mpaaeu  43139  icceuelpart  47437  isuspgrim0lem  47893