Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rspcv | Unicode version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.) |
Ref | Expression |
---|---|
rspcv.1 |
Ref | Expression |
---|---|
rspcv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1521 | . 2 | |
2 | rspcv.1 | . 2 | |
3 | 1, 2 | rspc 2828 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wcel 2141 wral 2448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ral 2453 df-v 2732 |
This theorem is referenced by: rspccv 2831 rspcva 2832 rspccva 2833 rspcdva 2839 rspc3v 2850 rr19.3v 2869 rr19.28v 2870 rspsbc 3037 rspc2vd 3117 intmin 3849 ralxfrALT 4450 ontr2exmid 4507 reg2exmidlema 4516 0elsucexmid 4547 funcnvuni 5265 acexmidlemcase 5846 tfrlem1 6285 tfrlem9 6296 oawordriexmid 6447 nneneq 6832 diffitest 6862 xpfi 6904 ordiso2 7009 exmidontriimlem3 7189 prnmaxl 7439 prnminu 7440 cauappcvgprlemm 7596 cauappcvgprlemladdru 7607 cauappcvgprlemladdrl 7608 caucvgsrlemcl 7740 caucvgsrlemfv 7742 caucvgsr 7753 axcaucvglemres 7850 lbreu 8850 nnsub 8906 supinfneg 9543 infsupneg 9544 ublbneg 9561 fzrevral 10050 seq3caopr3 10426 seq3id3 10452 recan 11062 cau3lem 11067 caubnd2 11070 climshftlemg 11254 subcn2 11263 climcau 11299 serf0 11304 sumdc 11310 isumrpcl 11446 clim2prod 11491 prodmodclem2 11529 ndvdssub 11878 zsupcllemex 11890 dfgcd3 11954 dfgcd2 11958 coprmgcdb 12031 coprmdvds1 12034 nprm 12066 dvdsprm 12080 coprm 12087 sqrt2irr 12105 pcmpt 12284 pcmptdvds 12286 pcfac 12291 prmpwdvds 12296 lidrididd 12625 dfgrp2 12721 cnpnei 12974 lmss 13001 txlm 13034 psmet0 13082 metss 13249 metcnp3 13266 mulc1cncf 13331 cncfco 13333 2sqlem6 13711 2sqlem10 13716 bj-indsuc 13925 bj-inf2vnlem2 13968 trirec0 14038 iswomni0 14045 |
Copyright terms: Public domain | W3C validator |