![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reurex | Structured version Visualization version GIF version |
Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.) |
Ref | Expression |
---|---|
reurex | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reu5 3366 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
2 | 1 | simplbi 496 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wrex 3060 ∃!wreu 3362 ∃*wrmo 3363 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 395 df-eu 2558 df-rex 3061 df-rmo 3364 df-reu 3365 |
This theorem is referenced by: 2reu2rex 3378 reu3 3720 reuxfr1d 3743 2rexreu 3755 sbcreu 3868 reu0 4354 2reu4 4521 tz6.26OLD 6353 weniso 7358 oawordex 8579 oaabs 8670 oaabs2 8671 supval2 9491 fisup2g 9504 fiinf2g 9536 nqerf 10964 qbtwnre 13226 modprm0 16802 issrgid 20183 isringid 20246 isringrng 20262 lspsneu 21100 frgpcyg 21567 qtophmeo 23809 pjthlem2 25454 dyadmax 25615 quotlem 26325 2sqreulem1 27472 2sqreunnlem1 27475 nfrgr2v 30202 2pthfrgrrn 30212 frgrncvvdeqlem9 30237 frgr2wwlkn0 30258 pjhthlem2 31322 cnlnadj 32009 2reu2rex1 32406 rmoxfrd 32418 cvmliftpht 35159 finorwe 37102 lcfl7N 41213 renegeulem 42080 resubeqsub 42140 requad1 47230 requad2 47231 uzlidlring 47648 lubeldm2 48326 glbeldm2 48327 |
Copyright terms: Public domain | W3C validator |