![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvral | Unicode version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
Ref | Expression |
---|---|
cbvral.1 |
![]() ![]() ![]() ![]() |
cbvral.2 |
![]() ![]() ![]() ![]() |
cbvral.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
cbvral |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2235 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2235 |
. 2
![]() ![]() ![]() ![]() | |
3 | cbvral.1 |
. 2
![]() ![]() ![]() ![]() | |
4 | cbvral.2 |
. 2
![]() ![]() ![]() ![]() | |
5 | cbvral.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 1, 2, 3, 4, 5 | cbvralf 2598 |
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-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 |
This theorem is referenced by: cbvralv 2604 cbvralsv 2615 cbviin 3790 frind 4203 ralxpf 4613 eqfnfv2f 5440 ralrnmpt 5480 dff13f 5587 ofrfval2 5909 fmpt2x 6008 cbvixp 6512 mptelixpg 6531 xpf1o 6640 indstr 9180 fsum3 10930 fsum00 11005 mertenslem2 11079 cnmpt11 12105 bj-bdfindes 12552 bj-findes 12584 |
Copyright terms: Public domain | W3C validator |