![]() |
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 1509 |
. 2
![]() ![]() ![]() ![]() | |
2 | rspcv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | rspc 2787 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-ral 2422 df-v 2691 |
This theorem is referenced by: rspccv 2790 rspcva 2791 rspccva 2792 rspcdva 2798 rspc3v 2809 rr19.3v 2827 rr19.28v 2828 rspsbc 2995 intmin 3799 ralxfrALT 4396 ontr2exmid 4448 reg2exmidlema 4457 0elsucexmid 4488 funcnvuni 5200 acexmidlemcase 5777 tfrlem1 6213 tfrlem9 6224 oawordriexmid 6374 nneneq 6759 diffitest 6789 xpfi 6826 ordiso2 6928 prnmaxl 7320 prnminu 7321 cauappcvgprlemm 7477 cauappcvgprlemladdru 7488 cauappcvgprlemladdrl 7489 caucvgsrlemcl 7621 caucvgsrlemfv 7623 caucvgsr 7634 axcaucvglemres 7731 lbreu 8727 nnsub 8783 supinfneg 9417 infsupneg 9418 ublbneg 9432 fzrevral 9916 seq3caopr3 10285 seq3id3 10311 recan 10913 cau3lem 10918 caubnd2 10921 climshftlemg 11103 subcn2 11112 climcau 11148 serf0 11153 sumdc 11159 isumrpcl 11295 clim2prod 11340 prodmodclem2 11378 ndvdssub 11663 zsupcllemex 11675 dfgcd3 11734 dfgcd2 11738 coprmgcdb 11805 coprmdvds1 11808 nprm 11840 dvdsprm 11853 coprm 11858 sqrt2irr 11876 cnpnei 12427 lmss 12454 txlm 12487 psmet0 12535 metss 12702 metcnp3 12719 mulc1cncf 12784 cncfco 12786 bj-indsuc 13297 bj-inf2vnlem2 13340 trirec0 13412 |
Copyright terms: Public domain | W3C validator |