Axiom ax-17 973

Description: Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 965, ax-4 975 through ax-9 967, ax-10o 1142, and ax-12 970 through ax-16 1212: in that system, we can derive any instance of ax-17 973 not containing wff variables by induction on formula length, using ax17eq 1213 and ax17el 1363 for the basis together hbn 1006, hbal 1007, and hbim 1009. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).

Assertion

Ref	Expression
ax-17	⊢ (φ → ∀xφ)

Distinct variable group:   φ,x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff φ
2		vx	. . 3 set x
3	1, 2	wal 956	. 2 wff ∀xφ
4	1, 3	wi 3	1 wff (φ → ∀xφ)

This axiom is referenced by:  ax4 974  a4imv 1209  ax16 1211  dveeq2 1214  19.23adv 1216  ax11a2 1218  equid1 1271  ax16i 1272  ax16ALT 1273  a4imev 1275  equvin 1277  albidv 1280  exbidv 1281  19.9v 1286  19.21v 1287  19.21aiv 1288  19.21adv 1290  19.20dv 1291  19.22dv 1292  19.23v 1295  19.23aiv 1297  19.27v 1300  19.28v 1301  19.36v 1302  19.36aiv 1303  19.37v 1305  19.41v 1307  19.42v 1310  cbvalv 1316  cbvexv 1317  cbval2 1318  cbvex2 1319  cbval2v 1320  cbvex2v 1321  cbvald 1322  eeanv 1325  nexdv 1328  cleljust 1330  equsb3lem 1331  equsb3 1332  elsb3 1333  dfsb7 1342  sb7f 1343  sbid2v 1345  exsb 1352  dvelim 1354  dvelimALT 1355  dveeq1 1356  dveel1 1358  dveel2 1359  ax15 1361  ax11el 1366  euf 1386  eubidv 1388  sb8eu 1392  mo 1395  euex 1396  euorv 1401  mo4f 1404  mo4 1405  eu5 1411  immo 1419  moimv 1421  moanim 1429  moanimv 1431  euanv 1434  mopick 1435  moexexv 1442  2mo 1450  2mos 1451  2eu4 1455  2eu6 1457  bm1.1 1465  cleqf 1563  hbel 1569  hbeleq 1570  abeq2 1571  abbidv 1580  clelab 1584  sbabel 1587  ralbidva 1662  rexbidva 1663  ralbidv 1666  rexbidv 1667  2ralbida 1680  2ralbidva 1681  rgen2a 1702  r19.20dva 1712  r19.21aiv 1716  r19.21v 1719  r19.21adv 1721  r19.22dv 1740  r19.12 1743  r19.23aiv 1746  r19.23adv 1749  hbrab 1776  ralcom2 1779  raleq1 1789  rexeq1 1790  reueq1 1791  cbvralf 1799  cbvrexf 1800  cbvral 1801  cbvrex 1802  cbvralv 1803  cbvrexv 1804  cbvreuv 1805  rabeq 1812  ceqsalv 1830  ceqsexv 1838  ceqsex2 1839  ceqsex2v 1840  vtocl 1845  vtoclgf 1849  vtoclg 1850  vtocl2gf 1852  vtocl2g 1853  vtoclgaf 1854  vtoclga 1855  cla4gf 1863  cla4gv 1865  cla4egv 1866  rcla4 1874  rcla4e 1875  rcla4v 1876  rcla4ev 1880  eqvincf 1887  ceqsexg 1890  ceqsexgv 1891  elabgt 1898  elabf 1899  elab 1900  elabg 1902  elrab 1908  cbvabv 1912  cbvrab 1913  cbvrabv 1914  mo2icl 1926  moi2 1927  moi 1928  reu2 1933  reu6 1935  sbhyp 1943  sbralie 1944  hbsbc1g 1951  hbsbc1 1952  hbsbc1v 1953  hbsbcg 1954  sbccog 1955  sbcco2 1956  sbc5g 1957  sbc6g 1958  sbcieg 1965  elrabsf 1967  elabs2 1968  cbvralsv 1971  cbvrexsv 1972  sbcbidv 1981  sbcel1gv 1984  sbcel2gv 1985  hbsbc1gd 1987  hbsbcgd 1988  sbcralt 1994  sbcralgf 1996  sbcralg 1998  sbcrexg 1999  sbcabel 2000  csbexg 2012  sbcel12g 2015  sbcel1g 2017  sbceq1dig 2018  sbcel2g 2019  sbceq2dig 2020  csbeq2dv 2023  hbcsb1g 2028  hbcsbg 2030  hbcsb1gd 2031  hbcsbgd 2032  csbieb 2034  csbie2t 2037  csbnestglem 2039  csbnest1g 2041  csbidmg 2043  csbco3g 2044  sbcco3g 2045  csbabg 2047  dfss2f 2064  uniiunlem 2136  ne0f 2292  ne0 2293  abn0 2295  hbif 2378  hbpw 2412  eusn 2451  hbuni 2514  eluniab 2518  hbint 2548  elintab 2549  ssintab 2555  intab 2565  cbviunv 2595  ssiun2s 2599  iunrab 2601  iunid 2608  iununi 2622  sbcbrg 2668  sbcbr12g 2669  sbcbr1g 2670  sbcbr2g 2671  opabbid 2675  opabbidv 2676  cbvopab 2678  cbvopabv 2679  cbvopab1 2680  cbvopab1s 2681  cbvopab1v 2682  csbopabg 2684  axrep1 2700  axrep2 2701  axrep3 2702  axrep4 2703  axrep5 2704  zfrepclf 2705  zfrep3cl 2706  axsep 2708  zfnuleu 2713  moabex 2773  copsex2g 2800  moop2 2808  mosubopt 2811  opabid 2817  hbopab 2819  opabsb 2822  dfid3 2843  euuni 2888  reuuni2f 2890  reuuni2 2891  reucl 2892  reucl2 2895  reusn 2899  alxfr 2903  ralxfrd 2904  ralxfr 2906  rabxfr 2909  reuunixfr 2913  onfr 2993  onminsb 3016  onminesb 3017  onminex 3027  tfis 3134  tfis2 3136  peano5 3160  findes 3167  tfinds 3168  tfindes 3171  tfinds2 3172  hbxp 3211  ralxp 3225  ralxpf 3227  hbrel 3252  hbco 3294  hbcnv 3302  dfdmf 3313  dfrnf 3355  hbrn 3358  dmcosseq 3372  hbres 3377  hbima 3418  csbima12g 3420  cnvopab 3452  dffun3 3534  dffunmof 3537  dffunmo 3538  hbfun 3543  funeu 3544  dffun7 3547  fun11 3569  imadif 3581  funimaexg 3582  isarep1 3584  isarep2 3585  fneu 3599  zfrep6 3621  fnopabg 3622  hbfv 3736  fv3 3740  tz6.12f 3745  tz6.12-2 3746  tz6.12c 3747  csbfv12g 3749  csbfv2g 3750  funfv2f 3779  fvopab4gf 3788  fvopab4s 3790  fvopabgf 3794  fvopabnf 3795  fvopab 3797  fvopab2 3798  fvopabs 3799  fvopab5 3800  eqfnfvf 3805  elrnopabg 3807  fopab2 3830  rnssopab 3832  ffnfv 3835  ffnfvf 3836  fopabco 3839  fopabcos 3840  fopabsn 3847  abrexexlem2 3866  funiunfvf 3877  abrexex2 3878  f1fvf 3882  cbvfo 3892  hbiso 3899  isotrALT 3905  iunon 3916  iinon 3917  tfrlem1 3918  tfr3 3933  hbrdg 3943  frsucopab 3961  tz7.48-1 3963  tz7.49 3966  abianfplem 3968  csboprg 3993  csbopr12g 3994  csbopr1g 3995  csbopr2g 3996  oprabbid 4002  oprabbidv 4003  cbvoprab12 4005  cbvoprab12v 4006  oprabval2gf 4033  oprabval2g 4034  oprabval4g 4038  2ndconst 4104  dfopab2 4120  dfoprab3 4121  dfoprab5 4122  foprab2 4126  elrnoprabg 4131  oawordeulem 4195  oarec 4203  eqerlem 4277  ixpf 4363  dom2d 4411  pw2en 4453  mapxpen 4502  xpmapenlem3 4505  xpmapenlem5 4507  nneneq 4519  pssnn 4546  unblem2 4554  unblem3 4555  unbnn 4557  fiint 4576  fiintOLD 4577  sucprcreg 4616  inf0 4622  trcl 4662  r1suc 4669  r1val1 4675  tz9.12lem3 4678  tz9.13g 4681  rankid 4689  rankuni2 4707  rankval4 4719  scottex 4733  scott0 4734  scottexs 4735  scott0s 4736  cp 4739  hta 4745  aceq1 4746  aceq5lem5 4756  ac6lem 4771  kmlem14 4795  kmlem15 4796  zorn2lem4 4808  zorn2lem5 4809  brdom3 4818  brdom7disj 4821  brdom6disj 4822  uniimadomf 4828  ondomcard 4875  cardmin 4878  cardprc 4879  alephon 4883  alephsuc 4884  alephordlem1 4890  cardaleph 4903  alephfplem2 4915  axrepndlem1 4963  axrepndlem2 4964  axunndlem1 4966  axunnd 4967  axpowndlem2 4969  axpowndlem4 4971  axregndlem2 4974  axinfnd 4977  axacndlem4 4981  axacndlem5 4982  zfcndrep 4985  zfcndpow 4987  zfcndinf 4989  zfcndac 4990  suppsrlem 5240  suppsr2 5242  suppsr3 5243  hbneg 5381  csbnegg 5383  nn1suc 5948  lble 6056  dfuz 6211  uzindOLD 6217  nn0ind-raph 6223  om2uzsuc 6304  seq1lem1 6317  uzind4s 6460  uzind4s2 6461  nnwof 6467  nnwos 6468  fzrevralt 6527  cau3i 6921  bccl2t 6978  hbsum1 6990  hbsum 6991  sumeq2 6992  fsumserzf 7007  fsum1f 7014  fsum1slem 7015  fsump1f 7018  fsump1slem 7019  fsum1p 7026  fsumconst 7045  ser1ser0 7055  binomlem1 7073  binomlem2 7074  binomlem4 7076  clm4le 7088  climeu 7107  iserzshft2 7114  climsup 7162  caucvglem6 7169  isumvaltf 7200  isumclimt 7203  isumclim2t 7206  isumnn0nna 7215  isummulc1 7219  isummulc1a 7221  isumcmpi 7222  infcvgaux1 7226  fnsmnt 7233  fsum0diaglem2 7264  fsum0diag 7265  fsum0diag2 7266  fsum0diag4 7268  tgval3t 7631  islp2 7751  cncnplem2 7779  iscaunns 7948  fsumcnlem 7993  minvecdist 8588  spwpr2 8661  grothprim 8785  chcmh 9115  cnlnadjlem5 10006  adjbdlnt 10018  rnbra 10042  atom1d 10283  irredt 10325  fine 10450  cmphmp 10515  homcard 10533  qusp 10549  fgsb 10563  fgsb2 10568  cnfilca 10570  cnvtr 10617  imonclem 10720  ismonc 10721  cmpmon 10722

Copyright terms: Public domain