| 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 2488 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 2 | sp 1533 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)) | |
| 3 | 1, 2 | sylbi 121 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∀wal 1370 ∈ wcel 2175 ∀wral 2483 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-4 1532 |
| This theorem depends on definitions: df-bi 117 df-ral 2488 |
| This theorem is referenced by: rspa 2553 rsp2 2555 rspec 2557 r19.12 2611 ralbi 2637 rexbi 2638 reupick2 3458 dfiun2g 3958 iinss2 3979 invdisj 4037 mpteq12f 4123 trss 4150 sowlin 4366 reusv1 4504 reusv3 4506 ralxfrALT 4513 funimaexglem 5356 fun11iun 5542 fvmptssdm 5663 ffnfv 5737 riota5f 5923 mpoeq123 6003 tfri3 6452 nneneq 6953 mkvprop 7259 cauappcvgprlemladdru 7768 cauappcvgprlemladdrl 7769 caucvgprlemm 7780 suplocexprlemss 7827 suplocsrlem 7920 indstr 9713 nninfinf 10586 prodeq2 11839 fprodle 11922 bezoutlemzz 12294 sgrpidmndm 13223 srgdilem 13702 ringdilem 13745 tgcl 14507 fsumcncntop 15010 dedekindeulemlu 15064 dedekindicclemlu 15073 bj-rspgt 15684 bj-charfunr 15708 |
| Copyright terms: Public domain | W3C validator |