Axiom ax-17 1007

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 999, ax-4 1009 through ax-9 1001, ax-10o 1177, and ax-12 1004 through ax-16 1247: in that system, we can derive any instance of ax-17 1007 not containing wff variables by induction on formula length, using ax17eq 1248 and ax17el 1400 for the basis together hbn 1040, hbal 1041, and hbim 1043. 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 990	. 2 wff ∀xφ
4	1, 3	wi 3	1 wff (φ → ∀xφ)

This axiom is referenced by:  ax4 1008  a4imv 1244  ax16 1246  dveeq2 1249  19.23adv 1251  ax11a2 1253  equid1 1307  ax16i 1308  ax16ALT 1309  a4imev 1311  equvin 1313  albidv 1316  exbidv 1317  19.9v 1322  19.21v 1323  19.21aiv 1324  19.21adv 1326  19.20dv 1327  19.22dv 1328  19.23v 1331  19.23aiv 1333  19.27v 1336  19.28v 1337  19.36v 1338  19.36aiv 1339  19.37v 1341  19.41v 1343  19.42v 1346  cbvalv 1352  cbvexv 1353  cbval2 1354  cbvex2 1355  cbval2v 1356  cbvex2v 1357  cbvald 1358  eeanv 1361  nexdv 1364  cleljust 1366  sbhb 1367  equsb3lem 1368  equsb3 1369  elsb3 1370  dfsb7 1379  sb7f 1380  sbid2v 1382  exsb 1389  dvelim 1391  dvelimALT 1392  dveeq1 1393  dveel1 1395  dveel2 1396  ax15 1398  ax11el 1403  euf 1423  eubidv 1425  sb8eu 1429  mo 1432  euex 1433  euorv 1438  mo4f 1441  mo4 1442  eu5 1448  immo 1456  moimv 1458  moanim 1466  moanimv 1468  euanv 1471  mopick 1472  moexexv 1479  2mo 1487  2mos 1488  2eu4 1492  2eu6 1494  bm1.1 1504  cleqf 1603  hbel 1609  hbeleq 1610  abeq2 1611  abbidv 1620  clelab 1624  sbabel 1627  ralbidva 1705  rexbidva 1706  ralbidv 1709  rexbidv 1710  2ralbida 1723  2ralbidva 1724  rgen2a 1745  r19.20dva 1755  r19.21aiv 1759  r19.21v 1762  r19.21adv 1764  r19.22dv 1783  r19.12 1786  r19.23aiv 1789  r19.23adv 1792  hbrab 1819  ralcom2 1822  raleq1 1832  rexeq1 1833  reueq1 1834  cbvralf 1842  cbvrexf 1843  cbvral 1844  cbvrex 1845  cbvralv 1846  cbvrexv 1847  cbvreuv 1848  rabeq 1855  ceqsalv 1873  ceqsexv 1881  ceqsex2 1882  ceqsex2v 1883  vtocl 1888  vtoclgf 1892  vtoclg 1893  vtocl2gf 1895  vtocl2g 1896  vtoclgaf 1897  vtoclga 1898  cla4gf 1906  cla4gv 1908  cla4egv 1909  rcla4 1917  rcla4e 1918  rcla4v 1919  rcla4ev 1923  eqvincf 1930  ceqsexg 1933  ceqsexgv 1934  elabgt 1941  elabf 1942  elab 1943  elabg 1945  elrab 1951  cbvabv 1955  cbvrab 1956  cbvrabv 1957  mo2icl 1969  moi2 1970  moi 1971  reu2 1976  reu6 1978  sbralie 1986  hbsbc1g 1993  hbsbc1 1994  hbsbc1v 1995  hbsbcg 1996  sbccog 1997  sbcco2 1998  sbc5g 1999  sbc6g 2000  sbcieg 2009  elrabsf 2011  elabs2 2012  cbvralsv 2015  cbvrexsv 2016  sbcbidv 2025  sbcel1gv 2028  sbcel2gv 2029  hbsbc1gd 2031  hbsbcgd 2032  sbc2ie 2036  sbc2iedv 2037  sbcralt 2040  sbcralgf 2042  sbcralg 2044  sbcrexg 2045  sbcabel 2046  csbexg 2059  sbcel12g 2062  sbcel1g 2064  sbceq1dig 2065  sbcel2g 2066  sbceq2dig 2067  csbeq2dv 2070  hbcsb1g 2075  hbcsbg 2077  hbcsb1gd 2078  hbcsbgd 2079  csbhypf 2080  csbieb 2082  csbie2t 2085  csbnestglem 2087  csbnest1g 2089  csbidmg 2091  csbco3g 2092  sbcco3g 2093  csbabg 2095  dfss2f 2112  uniiunlem 2184  ne0f 2340  n0 2341  abn0 2343  hbif 2427  hbpw 2464  eusn 2507  hbuni 2575  eluniab 2579  reucl 2584  hbint 2610  elintab 2611  ssintab 2617  intab 2627  cbviunv 2658  ssiun2s 2662  iunrab 2664  iununi 2686  sbcbrg 2736  sbcbr12g 2737  sbcbr1g 2738  sbcbr2g 2739  opabbid 2743  opabbidv 2744  cbvopab 2746  cbvopabv 2747  cbvopab1 2748  cbvopab1s 2749  cbvopab1v 2750  csbopabg 2752  axrep1 2768  axrep2 2769  axrep3 2770  axrep4 2771  axrep5 2772  zfrepclf 2773  zfrep3cl 2774  axsep 2776  zfnuleu 2781  moabex 2844  copsex2g 2869  moop2 2878  mosubopt 2881  opabid 2887  hbopab 2889  opelopabsb 2892  opelopabf 2899  dfid3 2914  posn 2928  onfr 3014  euuni 3105  reuuni2f 3107  reuuni2 3108  reucl2 3111  reusn 3115  alxfr 3119  ralxfrd 3120  ralxfr 3122  rabxfr 3125  reuunixfr 3129  onminsb 3155  onminesb 3156  onminex 3164  tfis 3208  tfis2 3210  tfinds 3212  tfindes 3215  tfinds2 3216  peano5 3241  findes 3248  hbxp 3287  ralxp 3301  ralxpf 3303  hbrel 3332  hbco 3377  hbcnv 3386  dfdmf 3397  dfrnf 3435  hbrn 3438  dmcosseq 3452  hbres 3457  hbima 3503  csbima12g 3505  cnvopab 3537  dffun3 3632  dffun6f 3635  dffun6 3636  hbfun 3641  funeu 3642  dffun8 3645  fun11 3667  imadif 3679  funimaexg 3681  isarep1 3683  isarep2 3684  fneu 3698  iunfopab 3719  zfrep6 3721  fnopabg 3722  hbfv 3840  fv3 3844  tz6.12f 3849  tz6.12-2 3850  tz6.12c 3851  csbfv12g 3853  csbfv2g 3854  funfv2f 3883  fvopab4gf 3892  fvopab4s 3894  fvopabgf 3898  fvopabnf 3899  fvopab 3901  fvopab2 3902  fvopabs 3903  fvopab5 3904  eqfnfvf2 3912  elrnopabg 3914  fopab2 3937  rnssopab 3939  ffnfv 3942  ffnfvf 3943  fopabco 3946  fopabcos 3947  fopabsn 3954  abrexexlem2 3973  funiunfvf 3984  abrexex2 3985  dff13f 3989  cbvfo 3999  hbiso 4006  isotrALT 4012  csboprg 4044  csbopr12g 4045  csbopr1g 4046  csbopr2g 4047  oprabbid 4054  oprabbidv 4055  cbvoprab1 4057  cbvoprab12 4058  cbvoprab12v 4059  oprabval2gf 4086  oprabval2g 4087  oprabval4g 4091  oprabval4gALT 4092  dfopab2 4173  dfoprab3 4174  dfoprab5sf 4178  foprab2 4181  elrnoprabg 4186  1stconst 4190  2ndconst 4191  iunfoprab 4192  fparlem1 4199  fparlem2 4200  iunon 4207  iinon 4208  onopriun 4211  tfrlem1 4212  tfr3 4227  hbrdg 4237  frsucopab 4255  tz7.48-1 4257  tz7.49 4260  abianfplem 4262  oawordeulem 4324  oarec 4332  eqerlem 4410  ixpf 4497  dom2d 4545  pw2en 4587  ac6sfilem1 4588  ac6sfilem3 4590  ac6sfi 4591  mapxpen 4642  xpmapenlem3 4645  xpmapenlem5 4647  nneneq 4659  pssnn 4681  unblem2 4687  unblem3 4688  unbnn 4690  fiint 4703  iunfi 4712  sucprcreg 4743  inf0 4751  trcl 4791  r1suc 4798  r1val1 4804  tz9.12lem3 4807  tz9.13g 4810  rankid 4818  rankuni2 4836  rankval4 4848  scottex 4862  scott0 4863  scottexs 4864  scott0s 4865  cp 4868  hta 4874  aceq1 4875  aceq5lem5 4885  ac6lem 4900  kmlem14 4924  kmlem15 4925  zorn2lem4 4937  zorn2lem5 4938  brdom3 4947  brdom7disj 4950  brdom6disj 4951  uniimadomf 4957  ondomcard 5007  cardmin 5010  cardprc 5011  alephon 5015  alephsuc 5016  alephordlem1 5022  cardaleph 5035  alephfplem2 5047  axrepndlem1 5098  axrepndlem2 5099  axunndlem1 5101  axunnd 5102  axpowndlem2 5104  axpowndlem4 5106  axregndlem2 5109  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  zfcndrep 5120  zfcndpow 5122  zfcndinf 5124  zfcndac 5125  suppsrlem 5375  suppsr2 5377  suppsr3 5378  hbneg 5516  csbnegg 5518  nn1suc 6084  lble 6215  dfuzi 6373  uzindOLD 6379  nn0ind-raph 6385  uzind4s 6579  uzind4s2 6580  nnwof 6586  nnwos 6587  fzrevral 6650  om2uzsuci 6659  seq1lem1 6674  cau3ii 7117  bccl2 7174  hbsum1 7186  hbsum 7187  sumeq2 7188  fsumserzfi 7203  fsum1fi 7210  fsum1slem 7211  fsump1fi 7214  fsump1slem 7215  fsum1p 7222  fsumconst 7241  ser1ser0i 7251  binomlem1 7269  binomlem2 7270  binomlem4 7272  clm4lei 7284  climeu 7303  iserzshft2i 7310  climsupi 7358  caucvglem6 7365  isumvaltfi 7397  isumclim 7400  isumclim2 7403  isumnn0nnai 7412  isummulc1 7416  isummulc1ai 7418  isumcmpii 7419  infcvgaux1i 7423  arisumi 7430  fsum0diaglem2 7462  fsum0diag 7463  fsum0diag2 7464  fsum0diag4 7466  tgval3 7837  islp2 7957  cncnplem2 7985  metequiv 8091  iscaunns 8155  fsumcnlem 8200  minvecdist 8845  spwpr2 8920  grothprim 9057  chcmhi 9389  cnlnadjlem5 10283  adjbdln 10295  rnbra 10320  atom1d 10561  irred 10604  fine 10736  imgfldref2 10768  tostos 10883  cmphmp 11027  homcard 11045  qusp 11068  fgsb 11082  fgsb2 11086  cnfilca 11088  bwt2 11123  cnvtr 11161  imonclem 11268  ismonc 11269  cmpmon 11270  iepiclem 11278  isepic 11279  eqeu 11394  subtr 11395  subtr2 11396  cbvcsb 11397  cbvsbc 11398  cbviinv 11402  finminlem 11418  inficlALT 11424  ordtypelem4 11430  ordtypelem5 11431  ordtypelem6 11432  ordtypelem7 11433  ordtype 11434  omsubsdomlem1 11440  omsubsdomlem2 11441  elomsubsd 11446  infenomsub 11450  hscptsscld 11491  alexsublem3 11498  topbasfne 11560  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  topmeet 11587  topjoin 11588  limfilcf 11683  gafo 11773  gapm 11784  sbmo 11787  morex 11804  opabex3 11806  oprabopabf 11807  oprabopab 11808  fnopabco 11810  oprabco 11811  abrexex2g 11825  firnfi3 11830  ac6gf 11841  indexa 11845  indexd 11846  indexf 11847  filbcmb 11857  sdclem2 11876  sdc 11877  fsumltisumi 11886  fsumleisumi 11889  isumclf 11891  fsumlt1 11894  mettrifi 11912  mettrifi2 11913  cncfres 11956  totbndbnd 12000  elsb3NEWlem 12222  elsb4lem 12223  elsb2lem 12225  elsb1 12229

Copyright terms: Public domain