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 3692

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 3369	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3691	. . 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 3078 ∃wrex 3088 ∃!wreu 3365 ∃*wrmo 3366

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 2566 df-eu 2596 df-clel 2837 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368

This theorem is used by: reuind 3714 oawordeulem 8545 fin23lem23 10332 nqereu 10942 receu 11887 lbreu 12193 cju 12242 fprodser 16042 divalglem9 16497 ndvdssub 16505 qredeu 16754 pj1eu 19829 efgredeu 19885 lspsneu 21316 qtopeu 23948 qtophmeo 24049 minveclem7 25669 ig1peu 26407 coeeu 26458 plydivalg 26536 nocvxmin 28028 tgsegconeu 28836 hlcgreu 28971 mirreu3 29013 trgcopyeu 29200 axcontlem2 29430 umgr2edg1 29679 umgr2edgneu 29682 usgredgreu 29686 uspgredg2vtxeu 29688 4cycl2vnunb 30778 frgr2wwlk1 30817 minvecolem7 31372 hlimreui 31728 riesz4i 32552 cdjreui 32921 xreceu 33375 cvmseu 35863 segconeu 36599 outsideofeu 36719 poimirlem4 38381 bfp 38582 exidu1 38614 rngoideu 38661 lshpsmreu 39990 cdleme 41441 lcfl7N 42382 mapdpg 42587 hdmap14lem6 42754 rediveud 43326 mpaaeu 43999 icceuelpart 48344 isuspgrim0lem 48817