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 3367	. 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 3076 ∃wrex 3086 ∃!wreu 3363 ∃*wrmo 3364

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 2564 df-eu 2594 df-clel 2835 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366

This theorem is used by: reuind 3711 oawordeulem 8544 fin23lem23 10331 nqereu 10941 receu 11886 lbreu 12192 cju 12241 fprodser 16039 divalglem9 16494 ndvdssub 16502 qredeu 16751 pj1eu 19826 efgredeu 19882 lspsneu 21313 qtopeu 23945 qtophmeo 24046 minveclem7 25666 ig1peu 26403 coeeu 26454 plydivalg 26532 nocvxmin 28023 tgsegconeu 28831 hlcgreu 28966 mirreu3 29008 trgcopyeu 29195 axcontlem2 29425 umgr2edg1 29674 umgr2edgneu 29677 usgredgreu 29681 uspgredg2vtxeu 29683 4cycl2vnunb 30773 frgr2wwlk1 30812 minvecolem7 31367 hlimreui 31723 riesz4i 32547 cdjreui 32916 xreceu 33370 cvmseu 35858 segconeu 36594 outsideofeu 36714 poimirlem4 38376 bfp 38577 exidu1 38609 rngoideu 38656 lshpsmreu 39985 cdleme 41436 lcfl7N 42377 mapdpg 42582 hdmap14lem6 42749 rediveud 43321 mpaaeu 43994 icceuelpart 48339 isuspgrim0lem 48812