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 3691

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 3370	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2		rmo4.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	rmo4 3690	. . 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 3079 ∃wrex 3089 ∃!wreu 3366 ∃*wrmo 3367

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148

This proof depends on definitions: df-bi 210 df-an 402 df-ex 1812 df-mo 2567 df-eu 2597 df-clel 2838 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369

This theorem is used by: reuind 3713 oawordeulem 8573 fin23lem23 10414 nqereu 11024 receu 11971 lbreu 12277 cju 12326 fprodser 16128 divalglem9 16583 ndvdssub 16591 qredeu 16845 pj1eu 19922 efgredeu 19978 lspsneu 21413 qtopeu 24047 qtophmeo 24148 minveclem7 25768 ig1peu 26505 coeeu 26556 plydivalg 26632 nocvxmin 28153 tgsegconeu 28961 hlcgreu 29096 mirreu3 29138 trgcopyeu 29325 axcontlem2 29555 umgr2edg1 29804 umgr2edgneu 29807 usgredgreu 29811 uspgredg2vtxeu 29813 4cycl2vnunb 30903 frgr2wwlk1 30942 minvecolem7 31497 hlimreui 31853 riesz4i 32677 cdjreui 33046 xreceu 33541 cvmseu 36162 segconeu 36903 outsideofeu 37023 poimirlem4 38682 bfp 38898 exidu1 38930 rngoideu 38977 lshpsmreu 40306 cdleme 41757 lcfl7N 42698 mapdpg 42903 hdmap14lem6 43070 rediveud 43634 mpaaeu 44292 icceuelpart 48657 isuspgrim0lem 49130