![]() |
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 1537 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rex 2381 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
3 | 1, 2 | sylibr 133 | 1 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∃wex 1436 ∈ wcel 1448 ∃wrex 2376 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-4 1455 |
This theorem depends on definitions: df-bi 116 df-rex 2381 |
This theorem is referenced by: rsp2e 2442 ssiun2 3803 tfrlem9 6146 tfrlemibxssdm 6154 tfr1onlembxssdm 6170 tfrcllembxssdm 6183 findcard2 6712 findcard2s 6713 prarloclemup 7204 prmuloc2 7276 ltaddpr 7306 aptiprlemu 7349 cauappcvgprlemopl 7355 cauappcvgprlemopu 7357 cauappcvgprlem2 7369 caucvgprlemopl 7378 caucvgprlemopu 7380 caucvgprlem2 7389 caucvgprprlem2 7419 |
Copyright terms: Public domain | W3C validator |