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 1501 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 1314 | 1 wff ∀𝑥𝜑 |
Colors of variables: wff set class |
This axiom is referenced by: gen2 1411 mpg 1412 mpgbi 1413 mpgbir 1414 hbth 1424 19.23h 1459 19.9ht 1605 stdpc6 1664 equveli 1717 cesare 2081 camestres 2082 calemes 2093 ceqsralv 2691 vtocl2 2715 euxfr2dc 2842 sbcth 2895 sbciegf 2912 csbiegf 3013 sbcnestg 3023 csbnestg 3024 csbnest1g 3025 int0 3755 mpteq2ia 3984 mpteq2da 3987 ssopab2i 4169 relssi 4600 xpidtr 4899 funcnvsn 5138 funinsn 5142 tfrlem7 6182 tfri1 6230 sucinc 6309 findcard 6750 findcard2 6751 findcard2s 6752 fiintim 6785 fisseneq 6788 frec2uzrand 10133 frec2uzf1od 10134 frecfzennn 10154 hashinfom 10479 zfz1iso 10539 fclim 11018 distop 12165 ch2var 12870 strcollnf 13079 |
Copyright terms: Public domain | W3C validator |