Axiom ax-gen 960

Description: Rule of Generalization. The postulated inference rule of pure 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 x = x, we can conclude ∀xx = x or even ∀yx = x. Theorem a4i 979 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.

Hypothesis

Ref	Expression
ax-g.1	⊢ φ

Assertion

Ref	Expression
ax-gen	⊢ ∀xφ

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. 2 set x
3	1, 2	wal 951	1 wff ∀xφ

This axiom is referenced by:  ax4 969  ax5o 971  ax5 973  ax6 976  gen2 980  mpg 983  hbth 998  stdpc6 1123  cbv3 1160  cbval 1161  ax11eq 1356  a12lem1 1369  euor2 1430  rgen2a 1691  r19.21v 1708  vtocl2 1834  elabgt 1886  mosub 1913  sbcth 1936  sbciegf 1950  sbcralg 1984  sbcrexg 1985  csbex 1999  csbiegf 2021  csbief 2022  csbnestglem 2025  csbnest1g 2027  csbco3g 2030  sbcco3g 2031  int0 2537  intab 2550  dtruALT 2738  ssopab2i 2812  ordom 3131  relssi 3238  eqrelriv 3241  dmcosseq 3349  funsn 3529  fconst 3643  fopabcos 3818  tfrlem7 3902  caoprmo 4056  pssnn 4513  unifi 4532  fiint 4534  fodomfi 4540  supmo 4550  inf0 4578  axinf2 4596  trcl 4617  brdom3 4773  axpowndlem2 4922  axpowndlem4 4924  axregndlem2 4927  axinfnd 4930  suppsr3 5196  fzshftralt 6454  fsumrev 6967  fsumshft 6969  fsum0diag2 7194  sn0top 7589  indistop 7590  distop 7591  fctop 7592  cctop 7594  htthlem12 8561  spwval2 8577  faimpex 10339

Copyright terms: Public domain