Theorem reu4 3703

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wral 3085  ∃wrex 3095  ∃!wreu 3374  ∃*wrmo 3375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573  df-eu 2603  df-clel 2844  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377

This theorem is referenced by:  reuind  3725  oawordeulem  8539  fin23lem23  10310  nqereu  10914  receu  11859  lbreu  12165  cju  12214  fprodser  16003  divalglem9  16459  ndvdssub  16467  qredeu  16716  pj1eu  19766  efgredeu  19822  lspsneu  21225  qtopeu  23842  qtophmeo  23943  minveclem7  25563  ig1peu  26301  coeeu  26351  plydivalg  26429  nocvxmin  27914  hlcgreu  28853  mirreu3  28893  trgcopyeu  29074  axcontlem2  29256  umgr2edg1  29502  umgr2edgneu  29505  usgredgreu  29509  uspgredg2vtxeu  29511  4cycl2vnunb  30582  frgr2wwlk1  30621  minvecolem7  31176  hlimreui  31532  riesz4i  32356  cdjreui  32725  xreceu  33182  cvmseu  35667  segconeu  36402  outsideofeu  36522  poimirlem4  38163  bfp  38363  exidu1  38395  rngoideu  38442  lshpsmreu  39773  cdleme  41224  lcfl7N  42165  mapdpg  42370  hdmap14lem6  42537  rediveud  43094  mpaaeu  43769  icceuelpart  48074  isuspgrim0lem  48547