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 3696

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 3373	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3695	. . 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 3081 ∃wrex 3091 ∃!wreu 3369 ∃*wrmo 3370

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 2148

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-mo 2569 df-eu 2599 df-clel 2840 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372

This theorem is used by: reuind 3718 oawordeulem 8545 fin23lem23 10325 nqereu 10931 receu 11876 lbreu 12182 cju 12231 fprodser 16028 divalglem9 16483 ndvdssub 16491 qredeu 16740 pj1eu 19812 efgredeu 19868 lspsneu 21299 qtopeu 23926 qtophmeo 24027 minveclem7 25647 ig1peu 26385 coeeu 26435 plydivalg 26513 nocvxmin 28001 hlcgreu 28943 mirreu3 28984 trgcopyeu 29170 axcontlem2 29372 umgr2edg1 29621 umgr2edgneu 29624 usgredgreu 29628 uspgredg2vtxeu 29630 4cycl2vnunb 30714 frgr2wwlk1 30753 minvecolem7 31308 hlimreui 31664 riesz4i 32488 cdjreui 32857 xreceu 33313 cvmseu 35807 segconeu 36542 outsideofeu 36662 poimirlem4 38334 bfp 38535 exidu1 38567 rngoideu 38614 lshpsmreu 39943 cdleme 41394 lcfl7N 42335 mapdpg 42540 hdmap14lem6 42707 rediveud 43264 mpaaeu 43937 icceuelpart 48245 isuspgrim0lem 48718