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 1459 | . 2 | |
2 | ax-17 1459 | . 2 | |
3 | cbvalv.1 | . 2 | |
4 | 1, 2, 3 | cbvexh 1678 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 wex 1421 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: eujust 1943 euind 2779 reuind 2795 r19.3rm 3330 r19.9rmv 3333 raaanlem 3346 raaan 3347 cbvopab2v 3855 bm1.3ii 3899 mss 3981 zfun 4189 xpiindim 4491 relop 4504 dmmrnm 4572 dmxpm 4573 dmcoss 4619 xpm 4765 cnviinm 4879 fv3 5218 fo1stresm 5808 fo2ndresm 5809 iinerm 6201 riinerm 6202 ac6sfi 6379 ltexprlemdisj 6796 ltexprlemloc 6797 recexprlemdisj 6820 climmo 10137 bdbm1.3ii 10682 |
Copyright terms: Public domain | W3C validator |