![]() |
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 1500 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | cbval.2 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | nfri 1500 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | cbval.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 2, 4, 5 | cbvalh 1727 |
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-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1438 |
This theorem is referenced by: sb8 1829 cbval2 1894 sb8eu 2013 abbi 2254 cleqf 2306 cbvralf 2651 ralab2 2852 cbvralcsf 3067 dfss2f 3093 elintab 3790 cbviota 5101 sb8iota 5103 dffun6f 5144 dffun4f 5147 mptfvex 5514 findcard2 6791 findcard2s 6792 |
Copyright terms: Public domain | W3C validator |