HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Axiom ax-17 969
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 1358 and ax-16 1208, this axiom is logically redundant since it is a metatheorem justified by induction on the number of primitive connectives in wff ph, using ax17eq 1209 and ax17el 1359 together hbn 1002, hbal 1003, and hbim 1005. 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
StepHypRef Expression
1 wph . 2 wff ph
2 vx . . 3 set x
31, 2wal 952 . 2 wff A.xph
41, 3wi 3 1 wff (ph -> A.xph)
Colors of variables: wff set class
This axiom is referenced by:  ax4 970  a4imv 1205  ax16 1207  dveeq2 1210  19.23adv 1212  ax11a2 1214  equid1 1267  ax16i 1268  ax16ALT 1269  a4imev 1271  equvin 1273  albidv 1276  exbidv 1277  19.9v 1282  19.21v 1283  19.21aiv 1284  19.21adv 1286  19.20dv 1287  19.22dv 1288  19.23v 1291  19.23aiv 1293  19.27v 1296  19.28v 1297  19.36v 1298  19.36aiv 1299  19.37v 1301  19.41v 1303  19.42v 1306  cbvalv 1312  cbvexv 1313  cbval2 1314  cbvex2 1315  cbval2v 1316  cbvex2v 1317  cbvald 1318  eeanv 1321  nexdv 1324  cleljust 1326  equsb3lem 1327  equsb3 1328  elsb3 1329  dfsb7 1338  sb7f 1339  sbid2v 1341  exsb 1348  dvelim 1350  dvelimALT 1351  dveeq1 1352  dveel1 1354  dveel2 1355  ax15 1357  ax11el 1362  euf 1382  eubidv 1384  sb8eu 1388  mo 1391  euex 1392  euorv 1397  mo4f 1400  mo4 1401  eu5 1407  immo 1415  moimv 1417  moanim 1425  moanimv 1427  euanv 1430  mopick 1431  moexexv 1437  2mo 1445  2mos 1446  2eu4 1450  2eu6 1452  bm1.1 1460  cleqf 1557  hbel 1563  hbeleq 1564  abeq2 1565  abbidv 1574  clelab 1578  sbabel 1581  ralbidva 1656  rexbidva 1657  ralbidv 1660  rexbidv 1661  2ralbida 1674  2ralbidva 1675  rgen2a 1696  r19.20dva 1706  r19.21aiv 1710  r19.21v 1713  r19.21adv 1715  r19.22dv 1734  r19.12 1737  r19.23aiv 1740  r19.23adv 1743  hbrab 1770  ralcom2 1773  raleq1 1783  rexeq1 1784  reueq1 1785  cbvralf 1793  cbvral 1794  cbvrex 1795  cbvralv 1796  cbvrexv 1797  cbvreuv 1798  rabeq 1805  ceqsalv 1823  ceqsexv 1831  ceqsex2 1832  ceqsex2v 1833  vtocl 1838  vtoclgf 1842  vtoclg 1843  vtocl2gf 1845  vtocl2g 1846  vtoclgaf 1847  vtoclga 1848  cla4gf 1856  cla4gv 1858  cla4egv 1859  rcla4 1867  rcla4e 1868  rcla4v 1869  rcla4ev 1873  eqvincf 1880  ceqsexg 1883  ceqsexgv 1884  elabgt 1891  elabf 1892  elab 1893  elabg 1895  elrab 1901  cbvabv 1905  cbvrab 1906  cbvrabv 1907  mo2icl 1919  moi2 1920  moi 1921  reu2 1926  reu6 1928  sbhyp 1936  sbralie 1937  hbsbc1g 1944  hbsbc1 1945  hbsbc1v 1946  hbsbcg 1947  sbccog 1948  sbcco2 1949  sbc5g 1950  sbc6g 1951  sbcieg 1957  elrabsf 1959  elabs2 1960  cbvralsv 1963  cbvrexsv 1964  sbcbidv 1973  sbcel1gv 1976  sbcel2gv 1977  hbsbc1gd 1979  hbsbcgd 1980  sbcralt 1986  sbcralgf 1988  sbcralg 1990  sbcrexg 1991  sbcabel 1992  csbexg 2004  sbcel12g 2007  sbcel1g 2009  sbceq1dig 2010  sbcel2g 2011  sbceq2dig 2012  csbeq2dv 2015  hbcsb1g 2020  hbcsbg 2022  hbcsb1gd 2023  hbcsbgd 2024  csbieb 2026  csbie2t 2029  csbnestglem 2031  csbnest1g 2033  csbidmg 2035  csbco3g 2036  sbcco3g 2037  csbabg 2039  dfss2f 2056  uniiunlem 2128  ne0f 2283  ne0 2284  abn0 2286  hbif 2369  hbpw 2403  eusn 2442  hbuni 2504  eluniab 2508  hbint 2538  elintab 2539  ssintab 2545  intab 2555  cbviunv 2585  ssiun2s 2589  iunrab 2591  iunid 2598  iununi 2611  sbcbrg 2657  sbcbr12g 2658  sbcbr1g 2659  sbcbr2g 2660  opabbid 2664  opabbidv 2665  cbvopab 2667  cbvopabv 2668  cbvopab1 2669  cbvopab1s 2670  cbvopab1v 2671  csbopabg 2673  axrep1 2689  axrep2 2690  axrep3 2691  axrep4 2692  axrep5 2693  zfrepclf 2694  zfrep3cl 2695  axsep 2697  zfnuleu 2702  moabex 2761  copsex2g 2788  moop2 2796  mosubopt 2799  opabid 2805  hbopab 2807  opabsb 2810  dfid3 2831  euuni 2876  reuuni2f 2878  reuuni2 2879  reucl 2880  reucl2 2883  reusn 2887  alxfr 2891  ralxfrd 2892  ralxfr 2894  rabxfr 2897  reuunixfr 2901  onfr 2981  onminsb 3004  onminesb 3005  onminex 3015  tfis 3122  tfis2 3124  peano5 3148  findes 3155  tfinds 3156  tfindes 3159  tfinds2 3160  hbxp 3199  ralxp 3213  ralxpf 3215  hbrel 3240  hbco 3282  hbcnv 3290  dfdmf 3301  dfrnf 3342  hbrn 3345  dmcosseq 3357  hbres 3362  hbima 3403  csbima12g 3405  cnvopab 3437  dffun3 3519  dffunmof 3522  dffunmo 3523  hbfun 3528  funeu 3529  dffun7 3532  fun11 3554  imadif 3566  funimaexg 3567  isarep1 3569  isarep2 3570  fneu 3584  zfrep6 3606  fnopabg 3607  hbfv 3720  fv3 3724  tz6.12f 3729  tz6.12-2 3730  tz6.12c 3731  csbfv12g 3733  csbfv2g 3734  funfv2f 3763  fvopab4gf 3772  fvopab4s 3774  fvopabgf 3778  fvopabnf 3779  fvopab 3781  fvopab2 3782  fvopabs 3783  fvopab5 3784  eqfnfvf 3789  elrnopabg 3791  fopab2 3814  rnssopab 3816  ffnfv 3819  ffnfvf 3820  fopabco 3823  fopabcos 3824  fopabsn 3831  abrexexlem2 3850  funiunfvf 3861  abrexex2 3862  f1fvf 3866  cbvfo 3876  hbiso 3883  isotrALT 3889  iunon 3900  iinon 3901  tfrlem1 3902  tfr3 3917  hbrdg 3927  frsucopab 3945  tz7.48-1 3947  tz7.49 3950  abianfplem 3952  csboprg 3977  csbopr12g 3978  csbopr1g 3979  csbopr2g 3980  oprabbid 3986  oprabbidv 3987  cbvoprab12 3989  cbvoprab12v 3990  oprabval2gf 4017  oprabval2g 4018  oprabval4g 4022  2ndconst 4087  dfopab2 4103  dfoprab3 4104  dfoprab5 4105  foprab2 4109  elrnoprabg 4114  oawordeulem 4178  oarec 4186  eqerlem 4260  ixpf 4346  dom2d 4391  pw2en 4432  mapxpen 4481  xpmapenlem3 4484  xpmapenlem5 4486  nneneq 4498  pssnn 4519  unblem2 4524  unblem3 4525  unbnn 4527  fiint 4540  iunfi 4549  sucprcreg 4580  inf0 4586  trcl 4625  r1suc 4632  r1val1 4638  tz9.12lem3 4641  tz9.13g 4644  rankid 4652  rankuni2 4670  rankval4 4682  scottex 4696  scott0 4697  scottexs 4698  scott0s 4699  cp 4702  hta 4708  aceq1 4709  aceq5lem5 4719  ac6lem 4734  kmlem14 4758  kmlem15 4759  zorn2lem4 4771  zorn2lem5 4772  brdom3 4781  brdom7disj 4784  brdom6disj 4785  uniimadomf 4791  ondomcard 4837  cardmin 4840  cardprc 4841  alephon 4845  alephsuc 4846  alephordlem1 4852  cardaleph 4865  alephfplem2 4877  axrepndlem1 4924  axrepndlem2 4925  axunndlem1 4927  axunnd 4928  axpowndlem2 4930  axpowndlem4 4932  axregndlem2 4935  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  zfcndrep 4946  zfcndpow 4948  zfcndinf 4950  zfcndac 4951  suppsrlem 5201  suppsr2 5203  suppsr3 5204  hbneg 5342  csbnegg 5344  nn1suc 5895  lble 6002  dfuz 6158  uzindOLD 6164  nn0ind-raph 6170  om2uzsuc 6241  seq1lem1 6254  uzind4s 6392  uzind4s2 6393  nnwof 6399  nnwos 6400  fzrevralt 6459  cau3i 6859  bccl2t 6917  hbsum1 6929  hbsum 6930  sumeq2 6931  fsumserzf 6946  fsum1f 6953  fsum1slem 6954  fsump1f 6957  fsump1slem 6958  fsum1p 6965  fsumconst 6984  ser1ser0 6994  binomlem1 7012  binomlem2 7013  binomlem4 7015  clm4le 7027  climeu 7045  iserzshft2 7052  climsup 7099  caucvglem6 7106  isumvaltf 7137  isumclimt 7140  isumclim2t 7142  isumnn0nna 7151  isummulc1 7155  isummulc1a 7157  isumcmpi 7158  infcvgaux1 7162  fnsmnt 7169  fsum0diaglem2 7200  fsum0diag 7201  fsum0diag2 7202  fsum0diag4 7204  tgval3t 7575  islp2 7697  cncnplem2 7725  fsumcnlem 7939  minvecdist 8529  grothprim 8722  chcmh 9052  cnlnadjlem5 9942  adjbdlnt 9954  rnbra 9978  atom1d 10217  irredt 10259  cbvrexf 10374  fine 10384  cmphmp 10444  homcard 10462  qusp 10466  fgsb 10480  fgsb2 10485  cnfilca 10487  cnvtr 10518  imonclem 10619  ismonc 10620  cmpmon 10621
Copyright terms: Public domain