Axiom ax-17 971

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 963, ax-4 973 through ax-9 965, ax-10o 1140, and ax-12 968 through ax-16 1210: in that system, we can derive any instance of ax-17 971 not containing wff variables by induction on formula length, using ax17eq 1211 and ax17el 1361 for the basis together hbn 1004, hbal 1005, and hbim 1007. 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 954	. 2 wff A.xph
4	1, 3	wi 3	1 wff (ph -> A.xph)

This axiom is referenced by:  ax4 972  a4imv 1207  ax16 1209  dveeq2 1212  19.23adv 1214  ax11a2 1216  equid1 1269  ax16i 1270  ax16ALT 1271  a4imev 1273  equvin 1275  albidv 1278  exbidv 1279  19.9v 1284  19.21v 1285  19.21aiv 1286  19.21adv 1288  19.20dv 1289  19.22dv 1290  19.23v 1293  19.23aiv 1295  19.27v 1298  19.28v 1299  19.36v 1300  19.36aiv 1301  19.37v 1303  19.41v 1305  19.42v 1308  cbvalv 1314  cbvexv 1315  cbval2 1316  cbvex2 1317  cbval2v 1318  cbvex2v 1319  cbvald 1320  eeanv 1323  nexdv 1326  cleljust 1328  equsb3lem 1329  equsb3 1330  elsb3 1331  dfsb7 1340  sb7f 1341  sbid2v 1343  exsb 1350  dvelim 1352  dvelimALT 1353  dveeq1 1354  dveel1 1356  dveel2 1357  ax15 1359  ax11el 1364  euf 1384  eubidv 1386  sb8eu 1390  mo 1393  euex 1394  euorv 1399  mo4f 1402  mo4 1403  eu5 1409  immo 1417  moimv 1419  moanim 1427  moanimv 1429  euanv 1432  mopick 1433  moexexv 1439  2mo 1447  2mos 1448  2eu4 1452  2eu6 1454  bm1.1 1462  cleqf 1560  hbel 1566  hbeleq 1567  abeq2 1568  abbidv 1577  clelab 1581  sbabel 1584  ralbidva 1659  rexbidva 1660  ralbidv 1663  rexbidv 1664  2ralbida 1677  2ralbidva 1678  rgen2a 1699  r19.20dva 1709  r19.21aiv 1713  r19.21v 1716  r19.21adv 1718  r19.22dv 1737  r19.12 1740  r19.23aiv 1743  r19.23adv 1746  hbrab 1773  ralcom2 1776  raleq1 1786  rexeq1 1787  reueq1 1788  cbvralf 1796  cbvrexf 1797  cbvral 1798  cbvrex 1799  cbvralv 1800  cbvrexv 1801  cbvreuv 1802  rabeq 1809  ceqsalv 1827  ceqsexv 1835  ceqsex2 1836  ceqsex2v 1837  vtocl 1842  vtoclgf 1846  vtoclg 1847  vtocl2gf 1849  vtocl2g 1850  vtoclgaf 1851  vtoclga 1852  cla4gf 1860  cla4gv 1862  cla4egv 1863  rcla4 1871  rcla4e 1872  rcla4v 1873  rcla4ev 1877  eqvincf 1884  ceqsexg 1887  ceqsexgv 1888  elabgt 1895  elabf 1896  elab 1897  elabg 1899  elrab 1905  cbvabv 1909  cbvrab 1910  cbvrabv 1911  mo2icl 1923  moi2 1924  moi 1925  reu2 1930  reu6 1932  sbhyp 1940  sbralie 1941  hbsbc1g 1948  hbsbc1 1949  hbsbc1v 1950  hbsbcg 1951  sbccog 1952  sbcco2 1953  sbc5g 1954  sbc6g 1955  sbcieg 1961  elrabsf 1963  elabs2 1964  cbvralsv 1967  cbvrexsv 1968  sbcbidv 1977  sbcel1gv 1980  sbcel2gv 1981  hbsbc1gd 1983  hbsbcgd 1984  sbcralt 1990  sbcralgf 1992  sbcralg 1994  sbcrexg 1995  sbcabel 1996  csbexg 2008  sbcel12g 2011  sbcel1g 2013  sbceq1dig 2014  sbcel2g 2015  sbceq2dig 2016  csbeq2dv 2019  hbcsb1g 2024  hbcsbg 2026  hbcsb1gd 2027  hbcsbgd 2028  csbieb 2030  csbie2t 2033  csbnestglem 2035  csbnest1g 2037  csbidmg 2039  csbco3g 2040  sbcco3g 2041  csbabg 2043  dfss2f 2060  uniiunlem 2132  ne0f 2287  ne0 2288  abn0 2290  hbif 2373  hbpw 2407  eusn 2446  hbuni 2509  eluniab 2513  hbint 2543  elintab 2544  ssintab 2550  intab 2560  cbviunv 2590  ssiun2s 2594  iunrab 2596  iunid 2603  iununi 2616  sbcbrg 2662  sbcbr12g 2663  sbcbr1g 2664  sbcbr2g 2665  opabbid 2669  opabbidv 2670  cbvopab 2672  cbvopabv 2673  cbvopab1 2674  cbvopab1s 2675  cbvopab1v 2676  csbopabg 2678  axrep1 2694  axrep2 2695  axrep3 2696  axrep4 2697  axrep5 2698  zfrepclf 2699  zfrep3cl 2700  axsep 2702  zfnuleu 2707  moabex 2766  copsex2g 2793  moop2 2801  mosubopt 2804  opabid 2810  hbopab 2812  opabsb 2815  dfid3 2836  euuni 2881  reuuni2f 2883  reuuni2 2884  reucl 2885  reucl2 2888  reusn 2892  alxfr 2896  ralxfrd 2897  ralxfr 2899  rabxfr 2902  reuunixfr 2906  onfr 2986  onminsb 3009  onminesb 3010  onminex 3020  tfis 3127  tfis2 3129  peano5 3153  findes 3160  tfinds 3161  tfindes 3164  tfinds2 3165  hbxp 3204  ralxp 3218  ralxpf 3220  hbrel 3245  hbco 3287  hbcnv 3295  dfdmf 3306  dfrnf 3348  hbrn 3351  dmcosseq 3365  hbres 3370  hbima 3411  csbima12g 3413  cnvopab 3445  dffun3 3527  dffunmof 3530  dffunmo 3531  hbfun 3536  funeu 3537  dffun7 3540  fun11 3562  imadif 3574  funimaexg 3575  isarep1 3577  isarep2 3578  fneu 3592  zfrep6 3614  fnopabg 3615  hbfv 3729  fv3 3733  tz6.12f 3738  tz6.12-2 3739  tz6.12c 3740  csbfv12g 3742  csbfv2g 3743  funfv2f 3772  fvopab4gf 3781  fvopab4s 3783  fvopabgf 3787  fvopabnf 3788  fvopab 3790  fvopab2 3791  fvopabs 3792  fvopab5 3793  eqfnfvf 3798  elrnopabg 3800  fopab2 3823  rnssopab 3825  ffnfv 3828  ffnfvf 3829  fopabco 3832  fopabcos 3833  fopabsn 3840  abrexexlem2 3859  funiunfvf 3870  abrexex2 3871  f1fvf 3875  cbvfo 3885  hbiso 3892  isotrALT 3898  iunon 3909  iinon 3910  tfrlem1 3911  tfr3 3926  hbrdg 3936  frsucopab 3954  tz7.48-1 3956  tz7.49 3959  abianfplem 3961  csboprg 3986  csbopr12g 3987  csbopr1g 3988  csbopr2g 3989  oprabbid 3995  oprabbidv 3996  cbvoprab12 3998  cbvoprab12v 3999  oprabval2gf 4026  oprabval2g 4027  oprabval4g 4031  2ndconst 4097  dfopab2 4113  dfoprab3 4114  dfoprab5 4115  foprab2 4119  elrnoprabg 4124  oawordeulem 4188  oarec 4196  eqerlem 4270  ixpf 4356  dom2d 4404  pw2en 4446  mapxpen 4495  xpmapenlem3 4498  xpmapenlem5 4500  nneneq 4512  pssnn 4534  unblem2 4541  unblem3 4542  unbnn 4544  fiint 4559  fiintOLD 4560  iunfiOLD 4569  sucprcreg 4600  inf0 4606  trcl 4645  r1suc 4652  r1val1 4658  tz9.12lem3 4661  tz9.13g 4664  rankid 4672  rankuni2 4690  rankval4 4702  scottex 4716  scott0 4717  scottexs 4718  scott0s 4719  cp 4722  hta 4728  aceq1 4729  aceq5lem5 4739  ac6lem 4754  kmlem14 4778  kmlem15 4779  zorn2lem4 4791  zorn2lem5 4792  brdom3 4801  brdom7disj 4804  brdom6disj 4805  uniimadomf 4811  ondomcard 4857  cardmin 4860  cardprc 4861  alephon 4865  alephsuc 4866  alephordlem1 4872  cardaleph 4885  alephfplem2 4897  axrepndlem1 4944  axrepndlem2 4945  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpowndlem4 4952  axregndlem2 4955  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  zfcndrep 4966  zfcndpow 4968  zfcndinf 4970  zfcndac 4971  suppsrlem 5221  suppsr2 5223  suppsr3 5224  hbneg 5362  csbnegg 5364  nn1suc 5939  lble 6047  dfuz 6202  uzindOLD 6208  nn0ind-raph 6214  om2uzsuc 6296  seq1lem1 6309  uzind4s 6452  uzind4s2 6453  nnwof 6459  nnwos 6460  fzrevralt 6519  cau3i 6914  bccl2t 6971  hbsum1 6983  hbsum 6984  sumeq2 6985  fsumserzf 7000  fsum1f 7007  fsum1slem 7008  fsump1f 7011  fsump1slem 7012  fsum1p 7019  fsumconst 7038  ser1ser0 7048  binomlem1 7066  binomlem2 7067  binomlem4 7069  clm4le 7081  climeu 7100  iserzshft2 7107  climsup 7155  caucvglem6 7162  isumvaltf 7193  isumclimt 7196  isumclim2t 7199  isumnn0nna 7208  isummulc1 7212  isummulc1a 7214  isumcmpi 7215  infcvgaux1 7219  fnsmnt 7226  fsum0diaglem2 7257  fsum0diag 7258  fsum0diag2 7259  fsum0diag4 7261  tgval3t 7625  islp2 7747  cncnplem2 7775  iscaunns 7944  fsumcnlem 7989  minvecdist 8585  spwpr2 8658  spwpr3OLD 8662  grothprim 8783  chcmh 9113  cnlnadjlem5 10004  adjbdlnt 10016  rnbra 10040  atom1d 10280  irredt 10322  fine 10449  fineOLD 10450  cmphmp 10521  homcard 10539  qusp 10555  fgsb 10570  fgsbOLD 10571  fgsb2 10580  cnfilca 10583  cnfilcaOLD 10584  cnvtr 10638  imonclem 10741  ismonc 10742  cmpmon 10743

Copyright terms: Public domain