![]() |
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 3068 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | exsimpr 1864 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∃wex 1773 ∈ wcel 2098 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-rex 3068 |
This theorem is referenced by: reu3 3724 rmo2i 3883 dffo5 7119 el2xpss 8047 nqerf 10961 supsrlem 11142 vdwmc2 16955 toprntopon 22847 isch3 31071 19.9d2rf 32290 volfiniune 33882 bnj594 34576 bnj1371 34693 bnj1374 34695 loop1cycl 34780 umgr2cycllem 34783 umgr2cycl 34784 dfrdg4 35580 bj-0nelsngl 36483 bj-ccinftydisj 36725 poimirlem25 37151 mblfinlem3 37165 mblfinlem4 37166 clsk3nimkb 43501 grumnudlem 43753 ismnushort 43769 stoweidlem57 45474 |
Copyright terms: Public domain | W3C validator |