![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-gen | Unicode version |
Description: Rule of Generalization.
The postulated inference rule of predicate
calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if
something is unconditionally true, then it is true for all values of a
variable. For example, if we have proved ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ax-g.1 |
![]() ![]() |
Ref | Expression |
---|---|
ax-gen |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. 2
![]() ![]() | |
2 | vx |
. 2
![]() ![]() | |
3 | 1, 2 | wal 1283 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: gen2 1380 mpg 1381 mpgbi 1382 mpgbir 1383 hbth 1393 19.23h 1428 19.9ht 1573 stdpc6 1632 equveli 1684 cesare 2047 camestres 2048 calemes 2059 ceqsralv 2639 vtocl2 2663 euxfr2dc 2786 sbcth 2837 sbciegf 2854 csbiegf 2955 sbcnestg 2964 csbnestg 2965 csbnest1g 2966 int0 3670 mpteq2ia 3884 mpteq2da 3887 ssopab2i 4060 relssi 4477 xpidtr 4765 funcnvsn 4995 funinsn 4999 tfrlem7 5986 tfri1 6034 sucinc 6109 findcard 6444 findcard2 6445 findcard2s 6446 fisseneq 6474 frec2uzrand 9539 frec2uzf1od 9540 frecfzennn 9560 hashinfom 9854 fclim 10334 ch2var 10838 strcollnf 11047 |
Copyright terms: Public domain | W3C validator |