reu4 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > reu4		Structured version Visualization version GIF version

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∀wral 3077 ∃wrex 3087 ∃!wreu 3364 ∃*wrmo 3365

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-mo 2565 df-eu 2595 df-clel 2836 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367

This theorem is used by: reuind 3711 oawordeulem 8562 fin23lem23 10404 nqereu 11014 receu 11961 lbreu 12267 cju 12316 fprodser 16116 divalglem9 16571 ndvdssub 16579 qredeu 16833 pj1eu 19910 efgredeu 19966 lspsneu 21401 qtopeu 24035 qtophmeo 24136 minveclem7 25756 ig1peu 26493 coeeu 26544 plydivalg 26620 nocvxmin 28141 tgsegconeu 28949 hlcgreu 29084 mirreu3 29126 trgcopyeu 29313 axcontlem2 29543 umgr2edg1 29792 umgr2edgneu 29795 usgredgreu 29799 uspgredg2vtxeu 29801 4cycl2vnunb 30891 frgr2wwlk1 30930 minvecolem7 31485 hlimreui 31841 riesz4i 32665 cdjreui 33034 xreceu 33488 cvmseu 36041 segconeu 36776 outsideofeu 36896 poimirlem4 38542 bfp 38758 exidu1 38790 rngoideu 38837 lshpsmreu 40166 cdleme 41617 lcfl7N 42558 mapdpg 42763 hdmap14lem6 42930 rediveud 43494 mpaaeu 44151 icceuelpart 48517 isuspgrim0lem 48990