Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rsp | Structured version Visualization version GIF version |
Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.) |
Ref | Expression |
---|---|
rsp | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ral 2917 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
2 | sp 2053 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑)) | |
3 | 1, 2 | sylbi 207 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1481 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-12 2047 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-ral 2917 |
This theorem is referenced by: rspa 2930 rspec 2931 r19.21bi 2932 rsp2 2936 r19.12 3063 reupick2 3913 rspn0 3934 dfiun2g 4552 iinss2 4572 invdisj 4638 trssOLD 4762 reusv1 4866 reusv1OLD 4867 reusv2lem1 4868 reusv2lem3 4871 reusv3 4876 ralxfrALT 4887 fvmptss 6292 ffnfv 6388 riota5f 6636 mpt2eq123 6714 peano5 7089 fun11iun 7126 wfrlem4 7418 wfrlem12 7426 tfr3 7495 tz7.48-1 7538 tz7.49 7540 nneneq 8143 scottex 8748 dfac2 8953 infpssrlem4 9128 fin23lem30 9164 fin23lem31 9165 hsmexlem2 9249 domtriomlem 9264 axdc3lem2 9273 axdc3lem4 9275 konigthlem 9390 winalim2 9518 nqereu 9751 dedekind 10200 dedekindle 10201 prodeq2ii 14643 vdwlem9 15693 mreiincl 16256 srgi 18511 ringi 18560 lbsextlem3 19160 lbsextlem4 19161 tgcl 20773 txindis 21437 alexsubALTlem3 21853 prdsxmslem2 22334 fsumcn 22673 lebnumlem1 22760 iscmet3lem1 23089 iscmet3lem2 23090 ovoliunlem2 23271 mbfimaopnlem 23422 limciun 23658 ftalem3 24801 ostth3 25327 mptelee 25775 ubthlem2 27727 aciunf1lem 29462 esumcvg 30148 bnj228 30803 bnj590 30980 bnj594 30982 bnj600 30989 bnj1128 31058 bnj1125 31060 bnj1145 31061 bnj1398 31102 bnj1417 31109 dfon2lem3 31690 dfon2lem7 31694 trpredmintr 31731 frr3g 31779 frrlem4 31783 frrlem11 31792 sslttr 31914 neibastop1 32354 unblimceq0lem 32497 unbdqndv2 32502 cover2 33508 upixp 33524 indexdom 33529 filbcmb 33535 mettrifi 33553 mpt2bi123f 33971 riotasvd 34242 glbconxN 34664 cdlemefr29exN 35690 cdlemk36 36201 mptfcl 37283 aomclem2 37625 hbtlem5 37698 gneispace 38432 trintALTVD 39116 trintALT 39117 refsumcn 39189 rfcnnnub 39195 choicefi 39392 mullimc 39848 mullimcf 39855 addlimc 39880 itgsubsticclem 40191 stoweidlem25 40242 stoweidlem52 40269 stoweidlem59 40276 stoweidlem62 40279 wallispilem3 40284 stirlinglem13 40303 fourierdlem73 40396 2reu1 41186 ffnafv 41251 iunord 42422 setrec1lem2 42435 |
Copyright terms: Public domain | W3C validator |