![]() |
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 3370 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
2 | rmo4.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
3 | 2 | rmo4 3635 | . . 3 ⊢ (∃*𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦)) |
4 | 3 | anbi2i 613 | . 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
5 | 1, 4 | bitri 267 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∀wral 3088 ∃wrex 3089 ∃!wreu 3090 ∃*wrmo 3091 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-10 2079 ax-11 2093 ax-12 2106 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clel 2846 df-ral 3093 df-rex 3094 df-reu 3095 df-rmo 3096 |
This theorem is referenced by: reuind 3655 oawordeulem 7983 fin23lem23 9548 nqereu 10151 receu 11088 lbreu 11394 cju 11437 fprodser 15166 divalglem9 15615 ndvdssub 15623 qredeu 15861 pj1eu 18583 efgredeu 18641 lspsneu 19620 qtopeu 22031 qtophmeo 22132 minveclem7 23744 ig1peu 24471 coeeu 24521 plydivalg 24594 hlcgreu 26109 mirreu3 26145 trgcopyeu 26297 axcontlem2 26457 umgr2edg1 26699 umgr2edgneu 26702 usgredgreu 26706 uspgredg2vtxeu 26708 4cycl2vnunb 27827 frgr2wwlk1 27866 minvecolem7 28441 hlimreui 28798 riesz4i 29624 cdjreui 29993 xreceu 30347 cvmseu 32108 nocvxmin 32769 segconeu 32993 outsideofeu 33113 poimirlem4 34337 bfp 34544 exidu1 34576 rngoideu 34623 lshpsmreu 35690 cdleme 37141 lcfl7N 38082 mapdpg 38287 hdmap14lem6 38454 mpaaeu 39146 icceuelpart 42969 |
Copyright terms: Public domain | W3C validator |