![]() |
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 1528 |
. 2
![]() ![]() ![]() ![]() | |
2 | rspcv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rspc 2835 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2739 |
This theorem is referenced by: rspccv 2838 rspcva 2839 rspccva 2840 rspcdva 2846 rspc3v 2857 rr19.3v 2876 rr19.28v 2877 rspsbc 3045 rspc2vd 3125 intmin 3864 ralxfrALT 4467 ontr2exmid 4524 reg2exmidlema 4533 0elsucexmid 4564 funcnvuni 5285 acexmidlemcase 5869 tfrlem1 6308 tfrlem9 6319 oawordriexmid 6470 nneneq 6856 diffitest 6886 xpfi 6928 ordiso2 7033 exmidontriimlem3 7221 prnmaxl 7486 prnminu 7487 cauappcvgprlemm 7643 cauappcvgprlemladdru 7654 cauappcvgprlemladdrl 7655 caucvgsrlemcl 7787 caucvgsrlemfv 7789 caucvgsr 7800 axcaucvglemres 7897 lbreu 8901 nnsub 8957 supinfneg 9594 infsupneg 9595 ublbneg 9612 fzrevral 10104 seq3caopr3 10480 seq3id3 10506 recan 11117 cau3lem 11122 caubnd2 11125 climshftlemg 11309 subcn2 11318 climcau 11354 serf0 11359 sumdc 11365 isumrpcl 11501 clim2prod 11546 prodmodclem2 11584 ndvdssub 11934 zsupcllemex 11946 dfgcd3 12010 dfgcd2 12014 coprmgcdb 12087 coprmdvds1 12090 nprm 12122 dvdsprm 12136 coprm 12143 sqrt2irr 12161 pcmpt 12340 pcmptdvds 12342 pcfac 12347 prmpwdvds 12352 lidrididd 12800 dfgrp2 12901 grpidinv2 12927 dfgrp3mlem 12967 issubg4m 13051 srgrz 13165 srglz 13166 srgisid 13167 islmodd 13381 cnpnei 13689 lmss 13716 txlm 13749 psmet0 13797 metss 13964 metcnp3 13981 mulc1cncf 14046 cncfco 14048 2sqlem6 14437 2sqlem10 14442 bj-indsuc 14650 bj-inf2vnlem2 14693 trirec0 14762 iswomni0 14769 neap0mkv 14786 |
Copyright terms: Public domain | W3C validator |