Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rsp | GIF version |
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.) |
Ref | Expression |
---|---|
rsp | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2398 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | sp 1473 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | sylbi 120 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 ∈ wcel 1465 ∀wral 2393 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-4 1472 |
This theorem depends on definitions: df-bi 116 df-ral 2398 |
This theorem is referenced by: rsp2 2459 rspec 2461 r19.12 2515 ralbi 2541 rexbi 2542 reupick2 3332 dfiun2g 3815 iinss2 3835 invdisj 3893 mpteq12f 3978 trss 4005 sowlin 4212 reusv1 4349 reusv3 4351 ralxfrALT 4358 funimaexglem 5176 fun11iun 5356 fvmptssdm 5473 ffnfv 5546 riota5f 5722 mpoeq123 5798 tfri3 6232 nneneq 6719 mkvprop 7000 cauappcvgprlemladdru 7432 cauappcvgprlemladdrl 7433 caucvgprlemm 7444 suplocexprlemss 7491 suplocsrlem 7584 indstr 9356 bezoutlemzz 11617 tgcl 12160 fsumcncntop 12652 dedekindeulemlu 12695 dedekindicclemlu 12704 bj-rspgt 12920 |
Copyright terms: Public domain | W3C validator |