![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbval | Unicode version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Ref | Expression |
---|---|
cbval.1 |
![]() ![]() ![]() ![]() |
cbval.2 |
![]() ![]() ![]() ![]() |
cbval.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbval |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbval.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfri 1467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | cbval.2 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | nfri 1467 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | cbval.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 2, 4, 5 | cbvalh 1694 |
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-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 |
This theorem depends on definitions: df-bi 116 df-nf 1405 |
This theorem is referenced by: sb8 1795 cbval2 1856 sb8eu 1973 abbi 2213 cleqf 2264 cbvralf 2606 ralab2 2801 cbvralcsf 3012 dfss2f 3038 elintab 3729 cbviota 5029 sb8iota 5031 dffun6f 5072 dffun4f 5075 mptfvex 5438 findcard2 6712 findcard2s 6713 |
Copyright terms: Public domain | W3C validator |