Theorem reu4 3705

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wral 3045  ∃wrex 3054  ∃!wreu 3354  ∃*wrmo 3355

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 2534  df-eu 2563  df-clel 2804  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357

This theorem is referenced by:  reuind  3727  oawordeulem  8521  fin23lem23  10286  nqereu  10889  receu  11830  lbreu  12140  cju  12189  fprodser  15922  divalglem9  16378  ndvdssub  16386  qredeu  16635  pj1eu  19633  efgredeu  19689  lspsneu  21040  qtopeu  23610  qtophmeo  23711  minveclem7  25342  ig1peu  26087  coeeu  26137  plydivalg  26214  nocvxmin  27697  hlcgreu  28552  mirreu3  28588  trgcopyeu  28740  axcontlem2  28899  umgr2edg1  29145  umgr2edgneu  29148  usgredgreu  29152  uspgredg2vtxeu  29154  4cycl2vnunb  30226  frgr2wwlk1  30265  minvecolem7  30819  hlimreui  31175  riesz4i  31999  cdjreui  32368  xreceu  32849  cvmseu  35270  segconeu  36006  outsideofeu  36126  poimirlem4  37625  bfp  37825  exidu1  37857  rngoideu  37904  lshpsmreu  39109  cdleme  40561  lcfl7N  41502  mapdpg  41707  hdmap14lem6  41874  rediveud  42438  mpaaeu  43146  icceuelpart  47441  isuspgrim0lem  47897