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 1484 | . 2 |
3 | cbvex.2 | . . 3 | |
4 | 3 | nfri 1484 | . 2 |
5 | cbvex.3 | . 2 | |
6 | 2, 4, 5 | cbvexh 1713 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wnf 1421 wex 1453 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: sb8e 1813 cbvex2 1874 cbvmo 2017 mo23 2018 clelab 2242 cbvrexf 2626 issetf 2667 eqvincf 2784 rexab2 2823 cbvrexcsf 3033 abn0m 3358 rabn0m 3360 euabsn 3563 eluniab 3718 cbvopab1 3971 cbvopab2 3972 cbvopab1s 3973 intexabim 4047 iinexgm 4049 opeliunxp 4564 dfdmf 4702 dfrnf 4750 elrnmpt1 4760 cbvoprab1 5811 cbvoprab2 5812 opabex3d 5987 opabex3 5988 seq3f1olemp 10243 fsum2dlemstep 11171 bdsepnfALT 13014 strcollnfALT 13111 |
Copyright terms: Public domain | W3C validator |