| 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 2223 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 2 | df-rex 3096 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 3 | 1, 2 | sylibr 237 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 400 ∃wex 1806 ∈ wcel 2149 ∃wrex 3095 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-12 2219 |
| This theorem depends on definitions: df-bi 210 df-ex 1807 df-rex 3096 |
| This theorem is referenced by: rsp2e 3289 2rmorex 3726 2reurex 3732 ssiun2 5016 reusv2lem3 5372 fvelimad 6949 tfrlem9 8372 findcard2 9149 isinf 9225 findcard3 9243 scott0 9860 ac6c4 10465 supaddc 12182 supadd 12183 supmul1 12184 supmul 12187 fsuppmapnn0fiub 14027 mreiincl 17648 restmetu 24696 bposlem3 27416 nosupbnd1 27844 nosupbnd2 27846 noinfbnd1 27859 noinfbnd2 27861 opphllem5 28991 pjpjpre 31712 atom1d 32646 iinabrex 32855 actfunsnf1o 34936 bnj1398 35367 cvmlift2lem12 35705 finminlem 36718 neibastop2lem 36760 iooelexlt 37896 relowlpssretop 37898 ralssiun 37941 disjlem18 39442 prtlem18 39541 pell14qrdich 43488 unielss 43837 eliuniin 45709 eliuniin2 45730 eliunid 45757 disjinfi 45802 iunmapsn 45825 infnsuprnmpt 45857 upbdrech 45916 limclner 46257 limsupre3uzlem 46341 climuzlem 46349 sge0iunmptlemre 47021 iundjiun 47066 meaiininclem 47092 isomenndlem 47136 ovnsubaddlem1 47176 vonioo 47288 vonicc 47291 smfaddlem1 47369 f1oresf1o2 47917 |
| Copyright terms: Public domain | W3C validator |