Theorem reu4 3714

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 3361	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3713	. . 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 3357  ∃*wrmo 3358

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 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2539  df-eu 2568  df-clel 2809  df-ral 3052  df-rex 3061  df-rmo 3359  df-reu 3360

This theorem is referenced by:  reuind  3736  oawordeulem  8566  fin23lem23  10340  nqereu  10943  receu  11882  lbreu  12192  cju  12236  fprodser  15965  divalglem9  16420  ndvdssub  16428  qredeu  16677  pj1eu  19677  efgredeu  19733  lspsneu  21084  qtopeu  23654  qtophmeo  23755  minveclem7  25387  ig1peu  26132  coeeu  26182  plydivalg  26259  nocvxmin  27742  hlcgreu  28597  mirreu3  28633  trgcopyeu  28785  axcontlem2  28944  umgr2edg1  29190  umgr2edgneu  29193  usgredgreu  29197  uspgredg2vtxeu  29199  4cycl2vnunb  30271  frgr2wwlk1  30310  minvecolem7  30864  hlimreui  31220  riesz4i  32044  cdjreui  32413  xreceu  32896  cvmseu  35298  segconeu  36029  outsideofeu  36149  poimirlem4  37648  bfp  37848  exidu1  37880  rngoideu  37927  lshpsmreu  39127  cdleme  40579  lcfl7N  41520  mapdpg  41725  hdmap14lem6  41892  mpaaeu  43174  icceuelpart  47450  isuspgrim0lem  47906