![]() |
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 2169 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rex 3068 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | sylibr 233 | 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 ax-5 1905 ax-6 1963 ax-7 2003 ax-12 2166 |
This theorem depends on definitions: df-bi 206 df-ex 1774 df-rex 3068 |
This theorem is referenced by: rsp2e 3273 2rmorex 3751 2reurex 3757 ssiun2 5054 reusv2lem3 5404 fvelimad 6971 tfrlem9 8412 findcard2 9195 isinf 9291 isinfOLD 9292 findcard2OLD 9315 findcard3 9316 findcard3OLD 9317 scott0 9917 ac6c4 10512 supaddc 12219 supadd 12220 supmul1 12221 supmul 12224 fsuppmapnn0fiub 13996 mreiincl 17583 restmetu 24499 bposlem3 27239 nosupbnd1 27667 nosupbnd2 27669 noinfbnd1 27682 noinfbnd2 27684 opphllem5 28575 pjpjpre 31249 atom1d 32183 iinabrex 32380 actfunsnf1o 34269 bnj1398 34698 cvmlift2lem12 34957 finminlem 35835 neibastop2lem 35877 iooelexlt 36874 relowlpssretop 36876 ralssiun 36919 disjlem18 38304 prtlem18 38381 pell14qrdich 42320 unielss 42677 eliuniin 44496 eliuniin2 44517 eliunid 44547 disjinfi 44595 iunmapsn 44620 infnsuprnmpt 44655 upbdrech 44716 limclner 45068 limsupre3uzlem 45152 climuzlem 45160 sge0iunmptlemre 45832 iundjiun 45877 meaiininclem 45903 isomenndlem 45947 ovnsubaddlem1 45987 vonioo 46099 vonicc 46102 smfaddlem1 46180 tworepnotupword 46301 f1oresf1o2 46700 |
Copyright terms: Public domain | W3C validator |