Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cbvex | Unicode version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
cbvex.1 | |
cbvex.2 | |
cbvex.3 |
Ref | Expression |
---|---|
cbvex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvex.1 | . . 3 | |
2 | 1 | nfri 1507 | . 2 |
3 | cbvex.2 | . . 3 | |
4 | 3 | nfri 1507 | . 2 |
5 | cbvex.3 | . 2 | |
6 | 2, 4, 5 | cbvexh 1743 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wnf 1448 wex 1480 |
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 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 |
This theorem depends on definitions: df-bi 116 df-nf 1449 |
This theorem is referenced by: sb8e 1845 cbvex2 1910 cbvmo 2054 mo23 2055 clelab 2292 cbvrexf 2686 issetf 2733 eqvincf 2851 rexab2 2892 cbvrexcsf 3108 abn0m 3434 rabn0m 3436 euabsn 3646 eluniab 3801 cbvopab1 4055 cbvopab2 4056 cbvopab1s 4057 intexabim 4131 iinexgm 4133 opeliunxp 4659 dfdmf 4797 dfrnf 4845 elrnmpt1 4855 cbvoprab1 5914 cbvoprab2 5915 opabex3d 6089 opabex3 6090 seq3f1olemp 10437 fsum2dlemstep 11375 bdsepnfALT 13771 strcollnfALT 13868 |
Copyright terms: Public domain | W3C validator |