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 3725

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∀wral 3057 ∃wrex 3066 ∃!wreu 3370 ∃*wrmo 3371

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101

This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 df-mo 2530 df-eu 2559 df-clel 2806 df-ral 3058 df-rex 3067 df-rmo 3372 df-reu 3373

This theorem is referenced by: reuind 3747 oawordeulem 8568 fin23lem23 10343 nqereu 10946 receu 11883 lbreu 12188 cju 12232 fprodser 15919 divalglem9 16371 ndvdssub 16379 qredeu 16622 pj1eu 19644 efgredeu 19700 lspsneu 21004 qtopeu 23613 qtophmeo 23714 minveclem7 25356 ig1peu 26102 coeeu 26152 plydivalg 26227 nocvxmin 27704 hlcgreu 28415 mirreu3 28451 trgcopyeu 28603 axcontlem2 28769 umgr2edg1 29017 umgr2edgneu 29020 usgredgreu 29024 uspgredg2vtxeu 29026 4cycl2vnunb 30093 frgr2wwlk1 30132 minvecolem7 30686 hlimreui 31042 riesz4i 31866 cdjreui 32235 xreceu 32639 cvmseu 34880 segconeu 35601 outsideofeu 35721 poimirlem4 37091 bfp 37291 exidu1 37323 rngoideu 37370 lshpsmreu 38575 cdleme 40027 lcfl7N 40968 mapdpg 41173 hdmap14lem6 41340 mpaaeu 42568 icceuelpart 46770 isuspgrim0lem 47163

	
		OSZAR »