|   | 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 3382 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∃wrex 3070 ∃!wreu 3378 ∃*wrmo 3379 | 
| 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 207 df-an 396 df-eu 2569 df-rex 3071 df-rmo 3380 df-reu 3381 | 
| This theorem is referenced by: 2reu2rex 3394 reu3 3733 reuxfr1d 3756 2rexreu 3768 sbcreu 3876 reu0 4361 2reu4 4523 tz6.26OLD 6369 weniso 7374 oawordex 8595 oaabs 8686 oaabs2 8687 supval2 9495 fisup2g 9508 fiinf2g 9540 nqerf 10970 qbtwnre 13241 modprm0 16843 issrgid 20201 isringid 20268 isringrng 20284 lspsneu 21125 frgpcyg 21592 qtophmeo 23825 pjthlem2 25472 dyadmax 25633 quotlem 26342 2sqreulem1 27490 2sqreunnlem1 27493 nfrgr2v 30291 2pthfrgrrn 30301 frgrncvvdeqlem9 30326 frgr2wwlkn0 30347 pjhthlem2 31411 cnlnadj 32098 2reu2rex1 32500 rmoxfrd 32512 cvmliftpht 35323 finorwe 37383 lcfl7N 41503 renegeulem 42399 resubeqsub 42459 requad1 47609 requad2 47610 uzlidlring 48151 reuxfr1dd 48726 lubeldm2 48853 glbeldm2 48854 upciclem4 48926 | 
| Copyright terms: Public domain | W3C validator |