Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspe | GIF version |
Description: Restricted specialization. (Contributed by NM, 12-Oct-1999.) |
Ref | Expression |
---|---|
rspe | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 19.8a 1577 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rex 2448 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | sylibr 133 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∃wex 1479 ∈ wcel 2135 ∃wrex 2443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 |
This theorem depends on definitions: df-bi 116 df-rex 2448 |
This theorem is referenced by: rsp2e 2515 ssiun2 3903 tfrlem9 6278 tfrlemibxssdm 6286 tfr1onlembxssdm 6302 tfrcllembxssdm 6315 findcard2 6846 findcard2s 6847 prarloclemup 7427 prmuloc2 7499 ltaddpr 7529 aptiprlemu 7572 cauappcvgprlemopl 7578 cauappcvgprlemopu 7580 cauappcvgprlem2 7592 caucvgprlemopl 7601 caucvgprlemopu 7603 caucvgprlem2 7612 caucvgprprlem2 7642 suplocexprlemrl 7649 suplocexprlemru 7651 suplocexprlemlub 7656 |
Copyright terms: Public domain | W3C validator |