![]() |
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 1538 |
. 2
![]() ![]() ![]() ![]() | |
2 | rspcv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rspc 2847 |
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 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-v 2751 |
This theorem is referenced by: rspccv 2850 rspcva 2851 rspccva 2852 rspcdva 2858 rspc3v 2869 rr19.3v 2888 rr19.28v 2889 rspsbc 3057 rspc2vd 3137 intmin 3876 ralxfrALT 4479 ontr2exmid 4536 reg2exmidlema 4545 0elsucexmid 4576 funcnvuni 5297 acexmidlemcase 5883 tfrlem1 6322 tfrlem9 6333 oawordriexmid 6484 nneneq 6870 diffitest 6900 xpfi 6942 ordiso2 7047 exmidontriimlem3 7235 prnmaxl 7500 prnminu 7501 cauappcvgprlemm 7657 cauappcvgprlemladdru 7668 cauappcvgprlemladdrl 7669 caucvgsrlemcl 7801 caucvgsrlemfv 7803 caucvgsr 7814 axcaucvglemres 7911 lbreu 8915 nnsub 8971 supinfneg 9608 infsupneg 9609 ublbneg 9626 fzrevral 10118 seq3caopr3 10494 seq3id3 10520 recan 11131 cau3lem 11136 caubnd2 11139 climshftlemg 11323 subcn2 11332 climcau 11368 serf0 11373 sumdc 11379 isumrpcl 11515 clim2prod 11560 prodmodclem2 11598 ndvdssub 11948 zsupcllemex 11960 dfgcd3 12024 dfgcd2 12028 coprmgcdb 12101 coprmdvds1 12104 nprm 12136 dvdsprm 12150 coprm 12157 sqrt2irr 12175 pcmpt 12354 pcmptdvds 12356 pcfac 12361 prmpwdvds 12366 lidrididd 12819 dfgrp2 12923 grpidinv2 12954 dfgrp3mlem 12994 issubg4m 13084 srgrz 13231 srglz 13232 srgisid 13233 islmodd 13477 rmodislmod 13535 rnglidlmcl 13664 cnpnei 13990 lmss 14017 txlm 14050 psmet0 14098 metss 14265 metcnp3 14282 mulc1cncf 14347 cncfco 14349 2sqlem6 14738 2sqlem10 14743 bj-indsuc 14951 bj-inf2vnlem2 14994 trirec0 15064 iswomni0 15071 neap0mkv 15089 |
Copyright terms: Public domain | W3C validator |