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 3146 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | exsimpr 1870 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
3 | 1, 2 | sylbi 219 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∃wex 1780 ∈ wcel 2114 ∃wrex 3141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-rex 3146 |
This theorem is referenced by: reu3 3720 rmo2i 3873 dffo5 6872 nqerf 10354 supsrlem 10535 vdwmc2 16317 toprntopon 21535 isch3 29020 19.9d2rf 30237 volfiniune 31491 bnj594 32186 bnj1371 32303 bnj1374 32305 loop1cycl 32386 umgr2cycllem 32389 umgr2cycl 32390 dfrdg4 33414 bj-0nelsngl 34285 bj-ccinftydisj 34497 poimirlem25 34919 mblfinlem3 34933 mblfinlem4 34934 clsk3nimkb 40397 grumnudlem 40628 stoweidlem57 42349 |
Copyright terms: Public domain | W3C validator |