Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-gen | GIF 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 𝑥 = 𝑥, we can conclude ∀𝑥𝑥 = 𝑥 or even ∀𝑦𝑥 = 𝑥. Theorem spi 1517 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
ax-g.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
ax-gen | ⊢ ∀𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 wff 𝜑 | |
2 | vx | . 2 setvar 𝑥 | |
3 | 1, 2 | wal 1330 | 1 wff ∀𝑥𝜑 |
Colors of variables: wff set class |
This axiom is referenced by: gen2 1427 mpg 1428 mpgbi 1429 mpgbir 1430 hbth 1440 19.23h 1475 19.9ht 1621 stdpc6 1680 equveli 1733 cesare 2104 camestres 2105 calemes 2116 ceqsralv 2720 vtocl2 2744 euxfr2dc 2873 sbcth 2926 sbciegf 2944 csbiegf 3048 sbcnestg 3058 csbnestg 3059 csbnest1g 3060 int0 3793 mpteq2ia 4022 mpteq2da 4025 ssopab2i 4207 relssi 4638 xpidtr 4937 funcnvsn 5176 funinsn 5180 tfrlem7 6222 tfri1 6270 sucinc 6349 findcard 6790 findcard2 6791 findcard2s 6792 fiintim 6825 fisseneq 6828 frec2uzrand 10209 frec2uzf1od 10210 frecfzennn 10230 hashinfom 10556 zfz1iso 10616 fclim 11095 distop 12293 ch2var 13145 strcollnf 13354 |
Copyright terms: Public domain | W3C validator |