![]() |
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 1590 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rex 2461 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | sylibr 134 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∃wex 1492 ∈ wcel 2148 ∃wrex 2456 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 |
This theorem depends on definitions: df-bi 117 df-rex 2461 |
This theorem is referenced by: rsp2e 2528 ssiun2 3931 tfrlem9 6322 tfrlemibxssdm 6330 tfr1onlembxssdm 6346 tfrcllembxssdm 6359 findcard2 6891 findcard2s 6892 prarloclemup 7496 prmuloc2 7568 ltaddpr 7598 aptiprlemu 7641 cauappcvgprlemopl 7647 cauappcvgprlemopu 7649 cauappcvgprlem2 7661 caucvgprlemopl 7670 caucvgprlemopu 7672 caucvgprlem2 7681 caucvgprprlem2 7711 suplocexprlemrl 7718 suplocexprlemru 7720 suplocexprlemlub 7725 |
Copyright terms: Public domain | W3C validator |