![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvabv | Unicode version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.) |
Ref | Expression |
---|---|
cbvabv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbvabv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1462 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfv 1462 |
. 2
![]() ![]() ![]() ![]() | |
3 | cbvabv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | cbvab 2205 |
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 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 |
This theorem is referenced by: cdeqab1 2818 difjust 2985 unjust 2987 injust 2989 uniiunlem 3093 dfif3 3386 pwjust 3407 snjust 3427 intab 3691 iotajust 4933 tfrlemi1 6029 tfr1onlemaccex 6045 tfrcllemaccex 6058 frecsuc 6104 nqprlu 7009 recexpr 7100 caucvgprprlemval 7150 caucvgprprlemnbj 7155 caucvgprprlemaddq 7170 caucvgprprlem1 7171 caucvgprprlem2 7172 axcaucvg 7338 bds 11085 |
Copyright terms: Public domain | W3C validator |