Axiom ax-17 968

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. If we allow the otherwise redundant ax-15 1353 and ax-16 1206, this axiom is logically redundant since it is a metatheorem justified by induction on the number of primitive connectives in wff φ, using ax17eq 1207 and ax17el 1354 together hbn 1001, hbal 1002, and hbim 1004. 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 951	. 2 wff ∀xφ
4	1, 3	wi 3	1 wff (φ → ∀xφ)

This axiom is referenced by:  ax4 969  a4imv 1203  ax16 1205  dveeq2 1208  19.23adv 1209  ax11a2 1211  equid1 1264  ax16i 1265  ax16ALT 1266  a4imev 1268  equvin 1270  albidv 1273  exbidv 1274  19.9v 1279  19.21v 1280  19.21aiv 1281  19.21adv 1283  19.20dv 1284  19.22dv 1285  19.23v 1288  19.23aiv 1290  19.27v 1293  19.28v 1294  19.36v 1295  19.36aiv 1296  19.37v 1298  19.41v 1300  19.42v 1303  cbvalv 1309  cbvexv 1310  cbval2 1311  cbvex2 1312  cbval2v 1313  cbvex2v 1314  cbvald 1315  eeanv 1318  nexdv 1321  cleljust 1323  equsb3lem 1324  equsb3 1325  elsb3 1326  dfsb7 1335  sb7f 1336  sbid2v 1338  exsb 1345  dvelim 1347  dveeq1 1348  dveel1 1349  dveel2 1350  ax15 1352  ax11el 1357  euf 1377  eubidv 1379  sb8eu 1383  mo 1386  euex 1387  euorv 1392  mo4f 1395  mo4 1396  eu5 1402  immo 1410  moimv 1412  moanim 1420  moanimv 1422  euanv 1425  mopick 1426  moexexv 1432  2mo 1440  2mos 1441  2eu4 1445  2eu6 1447  bm1.1 1455  cleqf 1552  hbel 1558  hbeleq 1559  abeq2 1560  abbidv 1569  clelab 1573  sbabel 1576  ralbidva 1651  rexbidva 1652  ralbidv 1655  rexbidv 1656  2ralbida 1669  2ralbidva 1670  rgen2a 1691  r19.20dva 1701  r19.21aiv 1705  r19.21v 1708  r19.21adv 1710  r19.22dv 1729  r19.12 1732  r19.23aiv 1735  r19.23adv 1738  hbrab 1765  ralcom2 1768  raleq1 1778  rexeq1 1779  reueq1 1780  cbvralf 1788  cbvral 1789  cbvrex 1790  cbvralv 1791  cbvrexv 1792  cbvreuv 1793  rabeq 1800  ceqsalv 1818  ceqsexv 1826  ceqsex2 1827  ceqsex2v 1828  vtocl 1833  vtoclgf 1837  vtoclg 1838  vtocl2gf 1840  vtocl2g 1841  vtoclgaf 1842  vtoclga 1843  cla4gf 1851  cla4gv 1853  cla4egv 1854  rcla4 1862  rcla4e 1863  rcla4v 1864  rcla4ev 1868  eqvincf 1875  ceqsexg 1878  ceqsexgv 1879  elabgt 1886  elabf 1887  elab 1888  elabg 1890  elrab 1896  cbvabv 1900  cbvrab 1901  cbvrabv 1902  mo2icl 1914  moi 1915  reu2 1920  reu6 1922  sbhyp 1930  sbralie 1931  hbsbc1g 1938  hbsbc1 1939  hbsbc1v 1940  hbsbcg 1941  sbccog 1942  sbcco2 1943  sbc5g 1944  sbc6g 1945  sbcieg 1951  elrabsf 1953  elabs2 1954  cbvralsv 1957  cbvrexsv 1958  sbcbidv 1967  sbcel1gv 1970  sbcel2gv 1971  hbsbc1gd 1973  hbsbcgd 1974  sbcralt 1980  sbcralgf 1982  sbcralg 1984  sbcrexg 1985  sbcabel 1986  csbexg 1998  sbcel12g 2001  sbcel1g 2003  sbceq1dig 2004  sbcel2g 2005  sbceq2dig 2006  csbeq2dv 2009  hbcsb1g 2014  hbcsbg 2016  hbcsb1gd 2017  hbcsbgd 2018  csbieb 2020  csbie2t 2023  csbnestglem 2025  csbnest1g 2027  csbidmg 2029  csbco3g 2030  sbcco3g 2031  csbabg 2033  dfss2f 2050  uniiunlem 2122  ne0f 2277  ne0 2278  abn0 2280  hbif 2363  hbpw 2397  eusn 2436  hbuni 2499  eluniab 2503  hbint 2533  elintab 2534  ssintab 2540  intab 2550  cbviunv 2580  ssiun2s 2584  iunrab 2586  iunid 2593  iununi 2606  sbcbrg 2652  sbcbr12g 2653  sbcbr1g 2654  sbcbr2g 2655  opabbid 2659  opabbidv 2660  cbvopab 2662  cbvopabv 2663  cbvopab1 2664  cbvopab1s 2665  cbvopab1v 2666  csbopabg 2668  axrep1 2684  axrep2 2685  axrep3 2686  axrep4 2687  axrep5 2688  zfrepclf 2689  zfrep3cl 2690  axsep 2692  zfnuleu 2697  moabex 2756  copsex2g 2783  moop2 2790  mosubopt 2793  opabid 2799  hbopab 2801  opabsb 2804  dfid3 2826  euuni 2871  reuuni2f 2873  reuuni2 2874  reucl 2875  reucl2 2878  reusn 2882  alxfr 2886  ralxfrd 2887  ralxfr 2889  rabxfr 2892  reuunixfr 2896  onfr 2976  onminsb 2999  onminesb 3000  onminex 3010  tfis 3117  tfis2 3119  peano5 3143  findes 3150  tfinds 3151  tfindes 3154  tfinds2 3155  hbxp 3194  ralxp 3208  ralxpf 3210  hbrel 3235  hbco 3276  hbcnv 3284  dfdmf 3295  dfrnf 3334  hbrn 3337  dmcosseq 3349  hbres 3354  hbima 3395  csbima12g 3397  cnvopab 3431  dffun3 3513  dffunmof 3516  dffunmo 3517  hbfun 3522  funeu 3523  dffun7 3526  fun11 3548  imadif 3560  funimaexg 3561  isarep1 3563  isarep2 3564  fneu 3578  zfrep6 3600  fnopabg 3601  hbfv 3714  fv3 3718  tz6.12f 3723  tz6.12-2 3724  tz6.12c 3725  csbfv12g 3727  csbfv2g 3728  funfv2f 3757  fvopab4gf 3766  fvopab4s 3768  fvopabgf 3772  fvopabnf 3773  fvopab 3775  fvopab2 3776  fvopabs 3777  fvopab5 3778  eqfnfvf 3783  elrnopabg 3785  fopab2 3808  rnssopab 3810  ffnfv 3813  ffnfvf 3814  fopabco 3817  fopabcos 3818  fopabsn 3825  abrexexlem2 3844  funiunfvf 3855  abrexex2 3856  f1fvf 3860  cbvfo 3870  hbiso 3877  isotrALT 3883  iunon 3894  iinon 3895  tfrlem1 3896  tfr3 3911  hbrdg 3921  frsucopab 3939  tz7.48-1 3941  tz7.49 3944  abianfplem 3946  csboprg 3971  csbopr12g 3972  csbopr1g 3973  csbopr2g 3974  oprabbid 3980  oprabbidv 3981  cbvoprab12 3983  cbvoprab12v 3984  oprabval2gf 4011  oprabval2g 4012  oprabval4g 4016  2ndconst 4081  dfopab2 4097  dfoprab3 4098  dfoprab5 4099  foprab2 4103  elrnoprabg 4108  oawordeulem 4172  oarec 4180  eqerlem 4254  ixpf 4340  dom2d 4385  pw2en 4426  mapxpen 4475  xpmapenlem3 4478  xpmapenlem5 4480  nneneq 4492  pssnn 4513  unblem2 4518  unblem3 4519  unbnn 4521  fiint 4534  iunfi 4543  sucprcreg 4572  inf0 4578  trcl 4617  r1suc 4624  r1val1 4630  tz9.12lem3 4633  tz9.13g 4636  rankid 4644  rankuni2 4662  rankval4 4674  scottex 4688  scott0 4689  scottexs 4690  scott0s 4691  cp 4694  hta 4700  aceq1 4701  aceq5lem5 4711  ac6lem 4726  kmlem14 4750  kmlem15 4751  zorn2lem4 4763  zorn2lem5 4764  brdom3 4773  brdom7disj 4776  brdom6disj 4777  uniimadomf 4783  ondomcard 4829  cardmin 4832  cardprc 4833  alephon 4837  alephsuc 4838  alephordlem1 4844  cardaleph 4857  alephfplem2 4869  axrepndlem1 4916  axrepndlem2 4917  axunndlem1 4919  axunnd 4920  axpowndlem2 4922  axpowndlem4 4924  axregndlem2 4927  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  zfcndrep 4938  zfcndpow 4940  zfcndinf 4942  zfcndac 4943  suppsrlem 5193  suppsr2 5195  suppsr3 5196  hbneg 5334  csbnegg 5336  nn1suc 5887  lble 5994  dfuz 6150  uzindOLD 6156  nn0ind-raph 6162  om2uzsuc 6233  seq1lem1 6246  uzind4s 6384  uzind4s2 6385  nnwof 6391  nnwos 6392  fzrevralt 6451  cau3i 6851  bccl2t 6909  hbsum1 6921  hbsum 6922  sumeq2 6923  fsumserzf 6938  fsum1f 6945  fsum1slem 6946  fsump1f 6949  fsump1slem 6950  fsum1p 6957  fsumconst 6976  ser1ser0 6986  binomlem1 7004  binomlem2 7005  binomlem4 7007  clm4le 7019  climeu 7037  iserzshft2 7044  climsup 7091  caucvglem6 7098  isumvaltf 7129  isumclimt 7132  isumclim2t 7134  isumnn0nna 7143  isummulc1 7147  isummulc1a 7149  isumcmpi 7150  infcvgaux1 7154  fnsmnt 7161  fsum0diaglem2 7192  fsum0diag 7193  fsum0diag2 7194  fsum0diag4 7196  tgval3t 7567  islp2 7688  cncnplem2 7714  fsumcnlem 7923  minvecdist 8516  grothprim 8722  chcmh 9034  cnlnadjlem5 9919  adjbdlnt 9931  rnbra 9953  atom1d 10188  irredt 10230  cbvrexf 10338  fine 10348  cmphmp 10408  homcard 10426  qusp 10430  fgsb 10444  fgsb2 10449  cnfilca 10451  cnvtr 10482  imonclem 10583  ismonc 10584  cmpmon 10585

Copyright terms: Public domain