![]() |
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 2460 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | sp 1511 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | sylbi 121 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1351 ∈ wcel 2148 ∀wral 2455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-4 1510 |
This theorem depends on definitions: df-bi 117 df-ral 2460 |
This theorem is referenced by: rspa 2525 rsp2 2527 rspec 2529 r19.12 2583 ralbi 2609 rexbi 2610 reupick2 3421 dfiun2g 3918 iinss2 3938 invdisj 3996 mpteq12f 4082 trss 4109 sowlin 4319 reusv1 4457 reusv3 4459 ralxfrALT 4466 funimaexglem 5298 fun11iun 5481 fvmptssdm 5599 ffnfv 5673 riota5f 5852 mpoeq123 5931 tfri3 6365 nneneq 6854 mkvprop 7153 cauappcvgprlemladdru 7652 cauappcvgprlemladdrl 7653 caucvgprlemm 7664 suplocexprlemss 7711 suplocsrlem 7804 indstr 9589 prodeq2 11558 fprodle 11641 bezoutlemzz 11995 sgrpidmndm 12753 srgdilem 13083 ringdilem 13126 tgcl 13435 fsumcncntop 13927 dedekindeulemlu 13970 dedekindicclemlu 13979 bj-rspgt 14398 bj-charfunr 14422 |
Copyright terms: Public domain | W3C validator |