![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexex | Structured version Visualization version GIF version |
Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.) |
Ref | Expression |
---|---|
rexex | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rex 3095 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | exsimpr 1914 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
3 | 1, 2 | sylbi 209 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∃wex 1823 ∈ wcel 2106 ∃wrex 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-rex 3095 |
This theorem is referenced by: reu3 3607 rmo2i 3743 dffo5 6640 nqerf 10087 supsrlem 10268 vdwmc2 16087 toprntopon 21137 clwlkclwwlkfOLD 27392 isch3 28684 19.9d2rf 29904 volfiniune 30905 bnj594 31595 bnj1371 31710 bnj1374 31712 dfrdg4 32661 bj-0nelsngl 33545 bj-ccinftydisj 33704 poimirlem25 34054 mblfinlem3 34068 mblfinlem4 34069 clsk3nimkb 39286 stoweidlem57 41193 |
Copyright terms: Public domain | W3C validator |