Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cbvexv | Unicode version |
Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
cbvalv.1 |
Ref | Expression |
---|---|
cbvexv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1419 | . 2 | |
2 | ax-17 1419 | . 2 | |
3 | cbvalv.1 | . 2 | |
4 | 1, 2, 3 | cbvexh 1638 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 wex 1381 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: eujust 1902 euind 2728 reuind 2744 r19.3rm 3310 r19.9rmv 3313 raaanlem 3326 raaan 3327 cbvopab2v 3834 bm1.3ii 3878 mss 3962 zfun 4171 xpiindim 4473 relop 4486 dmmrnm 4554 dmxpm 4555 dmcoss 4601 xpm 4745 cnviinm 4859 fv3 5197 fo1stresm 5788 fo2ndresm 5789 iinerm 6178 riinerm 6179 ac6sfi 6352 ltexprlemdisj 6704 ltexprlemloc 6705 recexprlemdisj 6728 climmo 9819 bdbm1.3ii 10011 |
Copyright terms: Public domain | W3C validator |