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 3371	. 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 3080 ∃wrex 3090 ∃!wreu 3367 ∃*wrmo 3368

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 1945 ax-6 2002 ax-7 2043 ax-8 2149

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-mo 2567 df-eu 2597 df-clel 2839 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370

This theorem is used by: reuind 3714 oawordeulem 8600 fin23lem23 10443 nqereu 11053 receu 12001 lbreu 12307 cju 12356 fprodser 16160 divalglem9 16615 ndvdssub 16623 qredeu 16877 pj1eu 19961 efgredeu 20017 lspsneu 21452 qtopeu 24090 qtophmeo 24191 minveclem7 25811 ig1peu 26548 coeeu 26599 plydivalg 26675 nocvxmin 28198 tgsegconeu 29006 hlcgreu 29141 mirreu3 29183 trgcopyeu 29370 axcontlem2 29600 umgr2edg1 29849 umgr2edgneu 29852 usgredgreu 29856 uspgredg2vtxeu 29858 4cycl2vnunb 30948 frgr2wwlk1 30987 minvecolem7 31542 hlimreui 31898 riesz4i 32722 cdjreui 33091 xreceu 33584 cvmseu 36249 segconeu 36991 outsideofeu 37111 poimirlem4 38810 bfp 39024 exidu1 39056 rngoideu 39103 lshpsmreu 40432 cdleme 41883 lcfl7N 42824 mapdpg 43029 hdmap14lem6 43196 rediveud 43760 mpaaeu 44417 icceuelpart 48791 isuspgrim0lem 49264