Axiom ax-gen 1143

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 A.xx = x or even A.yx = x. Theorem a4i 1166 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	|- ph

Assertion

Ref	Expression
ax-gen	|- A.xph

Detailed syntax breakdown of Axiom ax-gen

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. 2 set x
3	1, 2	wal 1134	1 wff A.xph

This axiom is referenced by:  hbequid 1151  equidqe 1152  equidq 1153  ax4 1156  ax5o 1158  ax5 1160  ax6 1163  gen2 1167  mpg 1170  mpgbi 1171  mpgbir 1172  hbth 1186  stdpc6 1324  cbv3 1363  cbvalOLD 1366  ax11eq 1592  a12lem1 1605  euor2OLD 1677  rgen2aOLD 1995  r19.21vOLD 2013  vtocl2 2173  vtocl2OLD 2174  elabgtOLD 2234  mosub 2266  sbcth 2291  sbciegf 2316  sbcralgOLD 2365  sbcrexgOLD 2367  csbexOLD 2383  csbiegf 2408  csbiefOLD 2410  csbnestglem 2413  csbnest1g 2415  csbco3g 2418  sbcco3g 2419  int0 3052  intab 3069  elOLD 3301  dtru 3313  ssopab2i 3389  ordom 3771  ordomOLD 3772  relssi 3889  eqrelrivOLD 3892  dmcosseqOLD 4026  funsn 4274  funsnOLD 4275  fconstOLD 4414  fopabcos 4617  caoprmo 4814  fparlem3 4894  fparlem4 4895  tfrlem7 4936  ac6sfilem3 5319  ac6sfi 5320  pssnn 5438  unifi 5458  fiint 5460  fodomfi 5466  supmo 5476  inf0 5521  axinf2 5539  trcl 5561  brdom3 5759  axpowndlem2 5898  axpowndlem4 5900  axregndlem2 5903  axinfnd 5906  suppsr3 6172  fzshftral 7496  fsumrev 8084  fsumshft 8086  fsum0diag2 8316  sn0top 8712  distop 8714  fctop 8715  cctop 8717  htthlem12 9773  spwval2 9791  findcard 9970  findcardOLD 9971  fbssint 10071  bnj226 12308  bnj897 12609  bnj920 12619  bnj1024 12671  bnj1022 12676  bnj889 13115  bnj1133 13218  hbimg 13667  wfrlem11 13759  allt 13881  alnof 13882  cpref 14102  lteqtpos 14352  invtrgrp 14693  elttar 14935  finsschain 15055  fneer 15178  neibastop1 15200  fcluscomplem 15302  unirep 15346  findcard2 15427  indexfi 15437  pm11.11 16005  sbc3orgVD 16334  hbra2VD 16343  isclati 16649

Copyright terms: Public domain