Axiom ax-17 1317

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 1305, ax-4 1319 through ax-9 1307, ax-10o 1500, and ax-12 1310 through ax-16 1580: in that system, we can derive any instance of ax-17 1317 not containing wff variables by induction on formula length, using ax17eq 1581 and ax17el 1752 for the basis together hbn 1351, hbal 1352, and hbim 1354. 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	|- (ph -> A.xph)

Distinct variable group:   ph,x

Detailed syntax breakdown of Axiom ax-17

Step	Hyp	Ref	Expression
1		wph	. 2 wff ph
2		vx	. . 3 set x
3	1, 2	wal 1296	. 2 wff A.xph
4	1, 3	wi 3	1 wff (ph -> A.xph)

This axiom is referenced by:  ax4 1318  a4imv 1576  ax16 1579  dveeq2 1582  19.23adv 1584  ax11a2 1586  equid1 1646  ax16i 1647  ax16ALT 1648  a4imev 1650  equvin 1652  albidv 1656  exbidv 1657  19.9v 1662  19.21v 1663  19.21aiv 1664  19.21adv 1666  alimdv 1668  eximdv 1669  19.23v 1672  19.23aiv 1674  19.27v 1677  19.28v 1678  19.36v 1679  19.36aiv 1680  19.12vv 1681  19.37v 1683  19.41v 1685  19.42v 1688  cbvalv 1696  cbvexv 1697  cbval2 1698  cbvex2 1699  cbval2v 1700  cbvex2v 1701  cbvald 1702  cbvaldOLD 1703  eeanv 1707  nexdv 1711  cleljust 1713  sbhb 1714  equsb3lem 1715  equsb3lemOLD 1716  equsb3 1717  elsb3 1718  elsb3OLD 1719  elsb4 1720  elsb4OLD 1721  dfsb7 1730  sb7fOLD 1732  sbid2v 1734  exsb 1741  dvelim 1743  dvelimALT 1744  dveeq1 1745  dveel1 1747  dveel2 1748  ax15 1750  ax11el 1755  eujustALT 1774  euf 1777  eubidv 1779  sb8eu 1783  sb8euOLD 1784  mo 1787  euex 1788  euexOLD 1789  euorv 1794  sbmo 1796  mo4f 1798  mo4 1799  eu5 1805  immo 1813  moimv 1815  moanim 1826  moanimv 1829  euanv 1832  mopick 1833  moexexv 1842  2mo 1851  2mos 1852  2eu4 1856  2eu6 1858  bm1.1 1870  cleqf 1984  eqsb3lem 1987  eqsb3lemOLD 1988  eqsb3 1989  clelsb3 1990  clelsb3OLD 1991  hbel 1996  hbeleq 1997  hbeleqOLD 1998  abeq2 1999  abbidv 2008  clelab 2013  sbabel 2016  ralbidva 2119  rexbidva 2120  ralbidv 2123  rexbidv 2124  2ralbida 2137  2ralbidva 2138  hbra2 2148  rgen2a 2160  rgen2aOLD 2161  ralimdvaa 2171  r19.21aiv 2175  r19.21v 2178  r19.21vOLD 2179  r19.21adv 2181  reximdvai 2201  r19.12 2204  r19.12OLD 2205  r19.23v 2208  r19.23aiv 2211  r19.23adv 2215  r19.41v 2236  ralcom2 2244  ralcom2OLD 2245  reean 2247  reeanOLD 2248  reeanv 2249  raleq 2266  rexeq 2267  reueq1 2268  cbvralf 2276  cbvrexf 2277  cbvral 2278  cbvrex 2279  cbvralv 2280  cbvrexv 2281  cbvreuv 2282  rabeq 2289  ceqsalv 2317  ceqsexv 2325  ceqsex2 2326  ceqsex2OLD 2327  ceqsex2v 2328  ceqsex2vOLD 2329  vtocl 2339  vtoclgf 2345  vtoclg 2346  vtocl2gf 2348  vtocl2g 2349  vtoclgaf 2350  vtoclgafOLD 2351  vtoclga 2352  cla4gf 2361  cla4gfOLD 2363  cla4gv 2364  cla4egv 2365  rcla4 2373  rcla4OLD 2374  rcla4e 2375  rcla4v 2376  rcla4ev 2381  eqvincf 2389  ceqsexg 2392  ceqsexgv 2393  elabgt 2400  elabgtOLD 2401  elabf 2402  elab 2403  elabg 2405  elab3g 2409  elrab 2414  cbvabv 2420  cbvrab 2421  cbvrabv 2422  abidhb 2423  mo2icl 2434  moi2 2435  moi 2436  reu2 2442  reu3 2444  sbralie 2453  hbsbc1 2462  hbsbc1OLD 2463  hbsbc1v 2464  hbsbc1vOLD 2465  sbccog 2467  sbcco2 2468  sbcco2OLD 2469  sbc5gOLD 2471  sbc6gOLD 2473  cbvsbcv 2480  sbcieg 2484  elrabsf 2486  elabs2 2487  cbvralsv 2490  cbvralsvOLD 2491  cbvrexsv 2492  cbvrexsvOLD 2493  sbcbidv 2505  sbcel1gvOLD 2511  sbcel2gv 2512  sbcel2gvOLD 2513  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  sbc2ie 2523  sbc2iedv 2524  sbcralt 2527  sbcralgf 2529  sbcralg 2531  sbcralgOLD 2532  sbcrexg 2533  sbcrexgOLD 2534  sbcabel 2535  csbexg 2548  sbcel12gOLD 2553  sbcel1g 2556  sbceq1dig 2557  sbcel2g 2558  sbceq2dig 2559  csbeq2dv 2562  hbcsb1g 2567  hbcsbg 2569  hbcsb1gd 2570  hbcsbgd 2571  csbhypf 2572  csbieb 2574  csbie2t 2578  csbnestglem 2580  csbnest1g 2582  csbidmg 2584  csbco3g 2585  sbcco3g 2586  csbabgOLD 2589  dfss2f 2612  ssralv2 2674  uniiunlem 2693  ne0f 2883  n0 2884  abn0 2892  raaan 2976  sbsslem 2978  sbsslemOLD 2979  sbss 2980  hbif 2999  hbifOLD 3000  hbpw 3041  euabsn 3095  hbuni 3183  hbuniOLD 3184  eluniab 3189  reucl 3213  hbint 3225  hbintOLD 3226  elintab 3227  ssintab 3233  ssintabOLD 3234  intab 3247  iineq2dv 3280  cbviunv 3290  ssiun2s 3297  iunrab 3299  iinab 3317  iinxsng 3325  iinxprg 3326  iununi 3331  iununiOLD 3332  brab1 3384  sbcbrg 3390  sbcbrgOLD 3391  sbcbr12g 3392  sbcbr1g 3393  sbcbr2g 3394  opabbidOLD 3400  opabbidv 3401  cbvopab 3403  cbvopabv 3404  cbvopab1 3405  cbvopab1s 3406  cbvopab1v 3407  csbopabg 3409  truni 3425  axrep1 3429  axrep2 3430  axrep3 3431  axrep4 3432  axrep5 3433  zfrepclf 3434  zfrep3cl 3435  axsep 3437  zfnuleu 3442  eunex 3500  moabex 3513  copsex2g 3539  moop2 3548  mosubopt 3551  opabidOLD 3558  hbopab 3560  hbopabOLD 3561  opelopabsbOLD 3565  opelopabf 3572  dfid3 3587  posn 3603  onfr 3702  euuni 3807  reuuni2f 3810  reuuni2 3811  reucl2 3814  reusn 3818  reusnOLD 3819  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq2 3829  eufromeq3 3830  eufromeq4 3831  eufromeq5 3832  eufromeq6 3833  euobj1 3834  alxfr 3836  ralxfrd 3837  ralxfr 3839  rabxfrd 3842  reuunixfr 3850  onminsb 3879  onminesb 3880  onminex 3888  tfis 3938  tfis2 3940  tfinds 3942  tfindsOLD 3943  tfindes 3946  tfinds2 3947  peano5 3975  findes 3983  hbxpOLD 4025  ralxp 4041  ralxpf 4043  hbrel 4073  hbco 4129  hbcnv 4139  dfdmf 4152  dfrnf 4195  hbrn 4198  hbrnOLD 4199  dmcosseqOLD 4215  hbres 4220  hbimaOLD 4274  csbima12g 4276  asymref2 4310  intirr 4312  cnvopabOLD 4318  dffun3 4432  dffun6f 4435  dffun6 4436  hbfun 4443  funeuOLD 4445  dffun8OLD 4449  fun11 4480  imadif 4493  funimaexg 4495  isarep1 4497  isarep1OLD 4498  isarep2 4499  fneuOLD 4518  iunfopabOLD 4543  zfrep6 4545  fnopabg 4546  hbfv 4686  fv3 4690  tz6.12f 4695  tz6.12-2 4696  tz6.12c 4697  csbfv12g 4699  csbfv2g 4700  funfv2f 4733  fvopab4gf 4744  fvopab4s 4746  fvopabgf 4750  fvopabnf 4751  fvopab 4753  fvopab2 4754  fvopabs 4755  fvopab5 4756  eqfnfv2f 4770  eufnfv 4771  elrnopabg 4773  fopab2 4796  rnssopab 4798  ffnfv 4801  ffnfvf 4802  fopabco 4805  fopabcos 4806  fopabsnOLD 4816  abrexexlem2 4835  funiunfvf 4846  abrexex2 4847  dff13f 4851  cbvfo 4861  hbiso 4868  hbisoOLD 4869  isotrALT 4875  csboprg 4910  csboprgOLD 4911  csbopr12g 4912  csbopr1g 4913  csbopr2g 4914  oprabbid 4921  oprabbidv 4922  cbvoprab1 4924  cbvoprab1OLD 4925  cbvoprab12 4926  cbvoprab12OLD 4927  cbvoprab12v 4928  oprabval2gf 4955  oprabval2g 4956  oprabval4g 4960  oprabval4gALT 4961  cbvmpt 5011  dfopab2 5053  dfoprab3 5054  dfoprab5sf 5058  foprab2 5061  elrnoprabg 5066  1stconst 5070  2ndconst 5071  iunfoprab 5072  fparlem1 5081  fparlem2 5082  hbiota1 5091  hbiota 5092  reiota2f 5109  reiota2 5110  iunon 5114  iinon 5115  onopriun 5118  tfrlem1 5119  tfr3 5134  hbrdg 5144  frsucopab 5162  tz7.48-1 5165  tz7.49 5168  abianfplem 5170  oawordeulem 5236  oarec 5244  eqerlem 5328  ixpf 5415  dom2d 5463  pw2en 5505  ac6sfilem1 5506  ac6sfilem3 5508  ac6sfi 5509  hbriota1 5569  hbriota 5570  riotacl2 5578  riota5 5580  riotaxfrd 5581  mapxpen 5589  xpmapenlem3 5592  xpmapenlem5 5594  nneneq 5606  pssnn 5628  unblem2 5634  unblem3 5635  unbnn 5637  fiint 5650  iunfi 5659  ordtypelem4 5687  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  sucprcreg 5703  inf0 5712  trcl 5752  r1suc 5763  r1val1 5769  tz9.12lem3 5772  tz9.13g 5775  rankid 5783  rankuni2 5801  rankval4 5813  19.21a3con13v 5828  scottex 5846  scott0 5847  scottexs 5848  scott0s 5849  cp 5852  hta 5858  alephon 5876  omsubsdomlem1 5879  omsubsdomlem2 5880  elomsubsd 5885  infenomsub 5889  aceq1 5891  aceq5lem5 5901  ac6lem 5916  kmlem14 5940  kmlem15 5941  zorn2lem4 5953  zorn2lem5 5954  brdom3 5963  brdom7disj 5966  brdom6disj 5967  uniimadomf 5973  ondomcard 6009  cardmin 6012  cardprc 6013  alephsuc 6014  alephordlem1 6020  cardaleph 6033  alephfplem2 6045  axrepndlem1 6096  axrepndlem2 6097  axunndlem1 6099  axunnd 6100  axpowndlem2 6102  axpowndlem4 6104  axregndlem2 6107  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  zfcndrep 6118  zfcndpow 6120  zfcndinf 6122  zfcndac 6123  suppsrlem 6373  suppsr2 6375  suppsr3 6376  hbneg 6517  hbnegd 6518  csbneggOLD 6521  subaddi 6528  divmuli 6894  nn1suc 7122  lble 7256  dfuzi 7414  uzindOLD 7420  nn0ind-raph 7426  uzind4s 7621  uzind4s2 7622  nnwof 7628  nnwos 7629  fzrevral 7698  om2uzsuci 7707  seq1lem1 7722  cau3ii 8166  bccl2 8223  hbsum1 8243  hbsum 8244  sumeq2 8245  fsumserzfi 8260  fsum1fi 8267  fsum1slem 8268  fsump1fi 8271  fsump1slem 8272  fsum1p 8279  fsumconst 8298  ser1ser0i 8308  binomlem1 8326  binomlem2 8327  binomlem4 8329  clm4lei 8341  climeu 8360  iserzshft2i 8367  climsupi 8415  caucvglem6 8422  isumvaltfi 8454  isumclim 8457  isumclim2 8460  isumnn0nnai 8469  isummulc1 8473  isummulc1ai 8475  isumcmpii 8476  infcvgaux1i 8480  arisumi 8487  fsum0diaglem2 8519  fsum0diag 8520  fsum0diag2 8521  fsum0diag4 8523  tgval3 8895  islp2 9023  cncnplem2 9052  metequiv 9158  iscaunns 9222  fsumcnlem 9267  gafo 9451  gapm 9462  minvecdist 9930  spwpr2 10001  grothprim 10141  oprabopabf 10157  oprabopab 10158  oprabco 10159  indexfi 10174  fine 10213  hausfillim2 10325  holimf 10326  chcmhi 10746  cnlnadjlem5 11641  adjbdln 11653  rnbra 11678  atom1d 11925  irred 11967  bnj14OLD 12382  bnj24 12388  bnj34 12403  bnj36OLD 12406  bnj37 12407  bnj37OLD 12408  bnj47 12417  bnj47OLD 12418  bnj48 12422  bnj48OLD 12423  bnj54 12428  bnj54OLD 12429  bnj55 12430  bnj58 12431  bnj62 12433  bnj77 12437  bnj79 12440  bnj90OLD 12446  bnj100 12449  bnj99 12450  bnj111OLD 12456  bnj112 12457  bnj131OLD 12463  bnj132OLD 12465  bnj220 12511  bnj525 12524  bnj853 12787  bnj870 12798  bnj876 12803  bnj912 12822  bnj921 12828  bnj919 12829  bnj1036 12886  bnj1096 12916  bnj1146 12943  bnj1216 12989  bnj1306 13049  bnj1310 13050  bnj1341 13066  bnj1346 13071  bnj1348 13072  bnj1349 13073  bnj1350 13074  bnj1351 13075  bnj1352 13076  bnj1353 13077  bnj1354 13078  bnj1355 13079  bnj1347 13080  bnj1357 13082  bnj1360 13085  bnj1366 13091  bnj1385 13102  bnj1400 13114  bnj1468 13145  bnj1479 13155  bnj1483 13160  bnj1492 13161  bnj1534 13183  bnj1542 13190  bnj65 13202  bnj81 13209  bnj82 13210  bnj86 13213  bnj87 13214  bnj91 13215  bnj92 13216  bnj109 13226  bnj119 13229  bnj121 13231  bnj124 13234  bnj130 13240  bnj154 13245  bnj155 13246  bnj207 13248  bnj571 13289  bnj573 13290  bnj578 13291  bnj605 13292  bnj594 13300  bnj580 13301  bnj607 13304  bnj611 13307  bnj75 13310  bnj873 13317  bnj849 13318  bnj900 13325  bnj894 13327  bnj911 13331  bnj916 13332  bnj958 13344  bnj965 13346  bnj964 13347  bnj981 13356  bnj983 13357  bnj985 13359  bnj1000 13364  bnj1014 13374  bnj1037 13386  bnj1093 13411  bnj1123 13422  bnj1129 13425  bnj1128 13428  bnj1145 13431  bnj1137 13433  bnj1228 13456  bnj1229 13457  bnj1268 13472  bnj1309 13487  bnj1307 13488  bnj1308 13489  bnj1313 13494  bnj1319 13495  bnj1321 13498  bnj1332 13499  bnj1375 13509  bnj1390 13513  bnj1398 13515  bnj1404 13517  bnj1417 13530  bnj1443 13533  bnj1445 13535  bnj1446 13536  bnj1447 13537  bnj1448 13538  bnj1449 13539  bnj1466 13548  bnj1467 13549  bnj1463 13550  bnj1482 13551  bnj1488 13553  bnj1491 13556  bnj1497 13560  bnj1499 13561  bnj1519 13568  bnj1520 13569  bnj1525 13572  bnj1529 13574  bnj1530 13575  lbzbi 13657  divalgb 13707  truniOLD 13792  untsucf 13798  setinds 13844  setinds2 13846  dfon2lem1 13849  dfon2lem3 13851  frsucopabn 13911  tfisg 13912  wfisg 13917  wfis2g 13921  trcllem1 13933  trcltr 13936  frinsg 13941  frins2g 13945  frins2 13946  soseq 13955  wfr3g 13956  frr3g 13980  sltval2 13997  axfelem4 14034  quantriv 14150  imgfldref2 14368  fopab2g 14485  hbcp 14500  npincppr 14501  repcpwti 14503  cbicplem 14508  unprj 14511  iserzmulc1b 14528  dutos1 14626  tostos 14637  isdir2 14640  hbprod1 14659  hbprod 14660  prodeq2 14661  fprodserzfi 14672  fprod1fi 14675  fprod1slem 14676  fprodp1fi 14680  fprodp1slem 14681  fprod1ib 14686  mgmlion 14697  fincmpzer 14711  fnopabco2b 14734  curgrpact 14735  fprodneg 14741  trooo 14758  cmprtr 14760  svli2 14826  cmphmp 14878  homcard 14893  stoig2b 14906  qusp 14908  fgsb 14921  fgsb2 14925  cnfilca 14927  bwt2 14960  trhom 14983  cntrsetlem 14999  cnvtr 15016  imonclem 15162  ismonc 15163  cmpmon 15164  iepiclem 15172  isepic 15173  tarval1 15214  tarval2 15249  btmp 15252  isline1 15294  eqeu 15351  subtr 15352  subtr2 15353  cbvcsb 15354  cbvsbcOLD 15355  cbviinv 15358  finminlem 15367  inficlALT 15372  ordtypelem4OLD 15378  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  omsubsdomlem1OLD 15388  omsubsdomlem2OLD 15389  elomsubsdOLD 15394  infenomsubOLD 15398  hscptsscld 15434  alexsublem3 15439  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop3 15524  topmeet 15526  topjoin 15527  limfilcf 15587  sbmoOLD 15654  unirep 15664  cover2 15673  opabex3 15701  cbvoprab2 15708  fnopabco 15711  cbvixp 15723  cbvixpv 15724  hbixp1 15725  abrexex2g 15738  firnfi3 15743  findcard2 15745  ac6gf 15749  indexa 15753  indexdom 15754  indexfiOLD 15755  pofun 15772  frminex 15773  filbcmb 15776  sdclem2 15810  sdc 15811  fdc1 15813  fsumltisumi 15823  fsumleisumi 15826  isumclf 15828  fsumlt1 15831  mettrifi 15847  mettrifi2 15848  oprpiece1res1 15880  oprpiece1res2 15881  cncfres 15895  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  totbndbnd 15944  prtlem5 16245  pm10.12 16304  19.31vv 16337  pm11.53 16344  aaanv 16345  pm11.57 16346  pm11.58 16347  pm11.59 16348  pm11.71 16354  ax10ext 16364  dvelimfALT2 16366  ax12 16367  pm13.192 16374  2sbc6g 16379  2sbc5g 16380  pm14.12 16385  cla4gft 16406  rcla4t 16407  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  compab 16418  cbviotaf 16432  cbviota 16433  smores 16446  ax172 16485  19.21a3con13vVD 16676  ssralv2VD 16690  elstrdiff 16720  elstrdif 16721  eustrdif 16722  stbval 16731  stb2xpl 16742  stb3xpl 16743  lubprop 16805  glbprop 16810  riotaoc 16936  glbconx 17029  pmapglbx 17251  pmapglb2x 17254

Copyright terms: Public domain