| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspe | Structured version Visualization version GIF version | ||
| Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
| Ref | Expression |
|---|---|
| rspe | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.8a 2181 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 2 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 3 | 1, 2 | sylibr 234 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∃wex 1779 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: rsp2e 3278 2rmorex 3760 2reurex 3766 ssiun2 5047 reusv2lem3 5400 fvelimad 6976 tfrlem9 8425 findcard2 9204 isinf 9296 isinfOLD 9297 findcard3 9318 findcard3OLD 9319 scott0 9926 ac6c4 10521 supaddc 12235 supadd 12236 supmul1 12237 supmul 12240 fsuppmapnn0fiub 14032 mreiincl 17639 restmetu 24583 bposlem3 27330 nosupbnd1 27759 nosupbnd2 27761 noinfbnd1 27774 noinfbnd2 27776 opphllem5 28759 pjpjpre 31438 atom1d 32372 iinabrex 32582 actfunsnf1o 34619 bnj1398 35048 cvmlift2lem12 35319 finminlem 36319 neibastop2lem 36361 iooelexlt 37363 relowlpssretop 37365 ralssiun 37408 disjlem18 38801 prtlem18 38878 pell14qrdich 42880 unielss 43230 eliuniin 45104 eliuniin2 45125 eliunid 45152 disjinfi 45197 iunmapsn 45222 infnsuprnmpt 45257 upbdrech 45317 limclner 45666 limsupre3uzlem 45750 climuzlem 45758 sge0iunmptlemre 46430 iundjiun 46475 meaiininclem 46501 isomenndlem 46545 ovnsubaddlem1 46585 vonioo 46697 vonicc 46700 smfaddlem1 46778 tworepnotupword 46901 f1oresf1o2 47303 |
| Copyright terms: Public domain | W3C validator |