![]() |
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 3370 | . 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑)) | |
2 | 1 | simplbi 490 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∃wrex 3089 ∃!wreu 3090 ∃*wrmo 3091 |
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 199 df-an 388 df-eu 2583 df-rex 3094 df-reu 3095 df-rmo 3096 |
This theorem is referenced by: 2reu2rex 3372 reu3 3632 reuxfr4d 3654 2rexreu 3664 sbcreu 3764 reu0 4206 2reu4 4350 reuxfrd 5175 tz6.26 6019 weniso 6932 oawordex 7986 oaabs 8073 oaabs2 8074 supval2 8716 fisup2g 8729 fiinf2g 8761 nqerf 10152 qbtwnre 12412 modprm0 16001 issrgid 18999 isringid 19049 lspsneu 19620 frgpcyg 20425 qtophmeo 22132 pjthlem2 23747 dyadmax 23905 quotlem 24595 2sqreulem1 25727 2sqreunnlem1 25730 nfrgr2v 27809 2pthfrgrrn 27819 frgrncvvdeqlem9 27844 frgr2wwlkn0 27865 pjhthlem2 28953 cnlnadj 29640 2reu2rex1 30029 rmoxfrd 30041 cvmliftpht 32150 lcfl7N 38082 renegeulem 38631 requad1 43156 requad2 43157 isringrng 43517 uzlidlring 43565 |
Copyright terms: Public domain | W3C validator |