![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reu4 | Structured version Visualization version GIF version |
Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
rmo4.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
reu4 | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reu5 3367 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
2 | rmo4.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | rmo4 3724 | . . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
4 | 3 | anbi2i 621 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
5 | 1, 4 | bitri 274 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∀wral 3051 ∃wrex 3060 ∃!wreu 3363 ∃*wrmo 3364 |
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 395 df-ex 1775 df-mo 2529 df-eu 2558 df-clel 2803 df-ral 3052 df-rex 3061 df-rmo 3365 df-reu 3366 |
This theorem is referenced by: reuind 3747 oawordeulem 8574 fin23lem23 10358 nqereu 10961 receu 11898 lbreu 12208 cju 12252 fprodser 15944 divalglem9 16396 ndvdssub 16404 qredeu 16652 pj1eu 19688 efgredeu 19744 lspsneu 21098 qtopeu 23706 qtophmeo 23807 minveclem7 25449 ig1peu 26197 coeeu 26247 plydivalg 26322 nocvxmin 27803 hlcgreu 28540 mirreu3 28576 trgcopyeu 28728 axcontlem2 28894 umgr2edg1 29142 umgr2edgneu 29145 usgredgreu 29149 uspgredg2vtxeu 29151 4cycl2vnunb 30218 frgr2wwlk1 30257 minvecolem7 30811 hlimreui 31167 riesz4i 31991 cdjreui 32360 xreceu 32784 cvmseu 35115 segconeu 35846 outsideofeu 35966 poimirlem4 37336 bfp 37536 exidu1 37568 rngoideu 37615 lshpsmreu 38818 cdleme 40270 lcfl7N 41211 mapdpg 41416 hdmap14lem6 41583 mpaaeu 42846 icceuelpart 47042 isuspgrim0lem 47484 |
Copyright terms: Public domain | W3C validator |