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 1452 | . 2 |
3 | cbvex.2 | . . 3 | |
4 | 3 | nfri 1452 | . 2 |
5 | cbvex.3 | . 2 | |
6 | 2, 4, 5 | cbvexh 1678 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 103 wnf 1389 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 df-nf 1390 |
This theorem is referenced by: sb8e 1778 cbvex2 1838 cbvmo 1981 mo23 1982 clelab 2203 cbvrexf 2572 issetf 2606 eqvincf 2720 rexab2 2758 cbvrexcsf 2965 rabn0m 3272 euabsn 3462 eluniab 3613 cbvopab1 3851 cbvopab2 3852 cbvopab1s 3853 intexabim 3927 iinexgm 3929 opeliunxp 4413 dfdmf 4546 dfrnf 4593 elrnmpt1 4603 cbvoprab1 5596 cbvoprab2 5597 opabex3d 5768 opabex3 5769 bdsepnfALT 10680 strcollnfALT 10781 |
Copyright terms: Public domain | W3C validator |