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 1484 | . 2 |
3 | cbval.2 | . . 3 | |
4 | 3 | nfri 1484 | . 2 |
5 | cbval.3 | . 2 | |
6 | 2, 4, 5 | cbvalh 1711 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1314 wnf 1421 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: sb8 1812 cbval2 1873 sb8eu 1990 abbi 2231 cleqf 2282 cbvralf 2625 ralab2 2821 cbvralcsf 3032 dfss2f 3058 elintab 3752 cbviota 5063 sb8iota 5065 dffun6f 5106 dffun4f 5109 mptfvex 5474 findcard2 6751 findcard2s 6752 |
Copyright terms: Public domain | W3C validator |