![]() |
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 1240 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: gen2 1336 mpg 1337 mpgbi 1338 mpgbir 1339 hbth 1349 19.23h 1384 19.9ht 1529 stdpc6 1588 equveli 1639 cesare 2001 camestres 2002 calemes 2013 ceqsralv 2579 vtocl2 2603 euxfr2dc 2720 sbcth 2771 sbciegf 2788 csbiegf 2884 sbcnestg 2893 csbnestg 2894 csbnest1g 2895 int0 3620 mpteq2ia 3834 mpteq2da 3837 ssopab2i 4005 relssi 4374 xpidtr 4658 funcnvsn 4888 tfrlem7 5874 tfri1 5892 sucinc 5964 frec2uzzd 8867 frec2uzsucd 8868 frec2uzrand 8872 frec2uzf1od 8873 frecfzennn 8884 ch2var 9242 strcollnf 9445 |
Copyright terms: Public domain | W3C validator |