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 1429 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 1241 | 1 wff ∀𝑥𝜑 |
Colors of variables: wff set class |
This axiom is referenced by: gen2 1339 mpg 1340 mpgbi 1341 mpgbir 1342 hbth 1352 19.23h 1387 19.9ht 1532 stdpc6 1591 equveli 1642 cesare 2004 camestres 2005 calemes 2016 ceqsralv 2585 vtocl2 2609 euxfr2dc 2726 sbcth 2777 sbciegf 2794 csbiegf 2890 sbcnestg 2899 csbnestg 2900 csbnest1g 2901 int0 3629 mpteq2ia 3843 mpteq2da 3846 ssopab2i 4014 relssi 4431 xpidtr 4715 funcnvsn 4945 tfrlem7 5933 tfri1 5951 sucinc 6025 findcard 6345 findcard2 6346 findcard2s 6347 frec2uzzd 9186 frec2uzsucd 9187 frec2uzrand 9191 frec2uzf1od 9192 frecfzennn 9203 fclim 9815 ch2var 9907 strcollnf 10110 |
Copyright terms: Public domain | W3C validator |