![]() |
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 1467 |
. 2
![]() ![]() ![]() ![]() | |
2 | rspcv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rspc 2717 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-v 2622 |
This theorem is referenced by: rspccv 2720 rspcva 2721 rspccva 2722 rspcdva 2728 rspc3v 2738 rr19.3v 2756 rr19.28v 2757 rspsbc 2922 intmin 3714 ralxfrALT 4302 ontr2exmid 4354 reg2exmidlema 4363 0elsucexmid 4394 funcnvuni 5096 acexmidlemcase 5661 tfrlem1 6087 tfrlem9 6098 oawordriexmid 6245 nneneq 6627 diffitest 6657 xpfi 6694 ordiso2 6782 prnmaxl 7108 prnminu 7109 cauappcvgprlemm 7265 cauappcvgprlemladdru 7276 cauappcvgprlemladdrl 7277 caucvgsrlemcl 7395 caucvgsrlemfv 7397 caucvgsr 7408 axcaucvglemres 7495 lbreu 8467 nnsub 8522 supinfneg 9144 infsupneg 9145 ublbneg 9159 fzrevral 9580 iseqval 9932 iseqfeq 9957 iseqcaopr3 9971 iseqid3s 9999 recan 10603 cau3lem 10608 caubnd2 10611 climshftlemg 10751 subcn2 10761 climcau 10797 serf0 10802 sumdc 10808 isumrpcl 10949 ndvdssub 11269 zsupcllemex 11281 dfgcd3 11338 dfgcd2 11342 coprmgcdb 11409 coprmdvds1 11412 nprm 11444 dvdsprm 11457 coprm 11462 sqrt2irr 11480 mulc1cncf 11918 cncfco 11920 bj-indsuc 12096 bj-inf2vnlem2 12139 |
Copyright terms: Public domain | W3C validator |