Axiom ax-17 1634

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 1622, ax-4 1637 through ax-9 1624, ax-10o 1810, and ax-12 1627 through ax-16 1883: in that system, we can derive any instance of ax-17 1634 not containing wff variables by induction on formula length, using ax17eq 1884 and ax17el 2045 for the basis together hbn 1669, hbal 1670, and hbim 1672. 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 1613	. 2 wff A.xph
4	1, 3	wi 3	1 wff (ph -> A.xph)

This axiom is referenced by:  a17d 1635  ax4 1636  a4imv 1880  ax16 1882  dveeq2 1885  dvelimfALT2 1887  19.23adv 1889  ax11a2 1891  equid1 1945  ax16i 1946  ax16ALT 1947  a4imev 1949  equvin 1951  albidv 1954  exbidv 1955  19.9v 1960  19.21v 1961  19.21aiv 1962  19.21adv 1964  alimdv 1966  eximdv 1967  19.23v 1970  19.23aiv 1972  19.27v 1975  19.28v 1976  19.36v 1977  19.36aiv 1978  19.12vv 1979  19.37v 1980  19.41v 1982  19.42v 1986  cbvalv 1993  cbvexv 1994  cbval2 1995  cbvex2 1996  cbval2v 1997  cbvex2v 1998  cbvald 1999  eeanv 2003  nexdv 2006  cleljust 2008  sbhb 2009  equsb3lem 2010  equsb3 2011  elsb3 2012  elsb4 2013  dfsb7 2024  sbid2v 2027  exsb 2034  dvelim 2036  dvelimALT 2037  dveeq1 2038  dveel1 2040  dveel2 2041  ax15 2043  ax11el 2048  a12study2 2064  eujustALT 2069  euf 2072  eubidv 2074  hbeud 2078  sb8eu 2079  mo 2082  euex 2083  euorv 2088  sbmo 2090  mo4f 2092  mo4 2093  eu5 2099  immo 2107  moimv 2109  moanim 2117  moanimv 2119  euanv 2122  mopick 2123  moexexv 2131  2mo 2139  2mos 2140  2eu4 2144  2eu6 2146  bm1.1 2156  cleqf 2264  eqsb3lem 2267  eqsb3 2268  clelsb3 2269  hbel 2275  hbeleq 2276  abeq2 2277  abbidv 2286  clelab 2291  sbabel 2294  ralbidva 2399  rexbidva 2400  ralbidv 2403  rexbidv 2404  2ralbida 2417  2ralbidva 2418  hbra2 2429  rgen2a 2441  ralimdva 2451  r19.21aiv 2455  r19.21v 2459  r19.21adv 2461  reximdvai 2481  r19.12 2484  r19.23v 2487  r19.23aiv 2489  r19.23adv 2493  r19.41v 2514  ralcom2 2521  reean 2523  reeanv 2524  raleq 2542  rexeq 2543  reueq1 2544  cbvralf 2553  cbvrexf 2554  cbvral 2555  cbvrex 2556  cbvralv 2557  cbvrexv 2558  cbvreuv 2559  rabeq 2566  issetf 2574  ceqsalv 2595  ceqsexv 2603  ceqsex2 2604  ceqsex2v 2605  vtocl 2614  vtoclgf 2618  vtoclg 2619  vtocl2gf 2621  vtocl2g 2622  vtoclgaf 2623  vtoclga 2624  cla4gf 2633  cla4gv 2635  cla4egv 2636  rcla4t 2644  rcla4 2645  rcla4e 2646  rcla4v 2647  rcla4ev 2651  rcla42 2654  rcla42v 2655  eqvincf 2660  ceqsexg 2663  ceqsexgv 2664  elabgt 2673  elabf 2674  elab 2675  elabg 2677  elab3g 2682  elrab 2685  cbvabv 2692  cbvrab 2693  cbvrabv 2694  abidhb 2695  mo2icl 2710  moi2 2711  moi 2712  reu2 2719  reu3 2721  sbralie 2730  hbsbc1 2738  hbsbc1v 2739  sbccog 2741  sbcco2 2742  cbvsbcv 2750  sbcieg 2754  elrabsf 2756  elabs2 2757  cbvralsv 2760  cbvrexsv 2761  sbcbidv 2774  sbcel2gv 2779  sbcg 2785  sbc2ie 2787  sbc2iedv 2788  sbcralgf 2793  sbcralg 2795  sbcrexg 2796  sbcreug 2797  sbcabel 2798  rmo3 2803  rmoi 2804  csbexg 2813  csbconstgfv 2816  sbcel1g 2819  sbceq1g 2820  sbcel2g 2821  sbceq2g 2822  csbeq2dv 2825  hbcsb1g 2830  hbcsbg 2832  hbcsbgd 2834  csbhypf 2835  csbieb 2837  csbie2t 2841  csbnestglem 2843  csbnest1g 2845  csbidmg 2847  csbco3g 2848  sbcco3g 2849  cbvralcsf 2852  cbvrexcsf 2853  cbvreucsf 2854  cbvrabcsf 2855  dfss2f 2875  uniiunlem 2950  csbing 3045  n0f 3122  n0 3123  abn0 3131  raaan 3208  sbsslem 3210  sbss 3211  hbif 3228  hbifd 3229  csbifg 3230  hbpw 3267  euabsn 3317  hbuni 3404  hbunid 3405  eluniab 3410  reucl 3431  hbint 3442  elintab 3443  ssintab 3449  intab 3460  iineq2dv 3488  cbviunv 3497  cbviinv 3498  ssiun2s 3502  iunrab 3504  ssiinf 3507  ssiin 3508  iinab 3519  iinxsng 3527  iinxprg 3528  iununi 3533  brab1 3588  sbcbrg 3593  sbcbr12g 3594  sbcbr1g 3595  sbcbr2g 3596  opabbidv 3601  cbvopab 3603  cbvopabv 3604  cbvopab1 3605  cbvopab1s 3606  cbvopab1v 3607  csbopabg 3609  truni 3624  axrep1 3629  axrep2 3630  axrep3 3631  axrep4 3632  axrep5 3633  zfrepclf 3634  zfrep3cl 3635  axsep 3637  zfnuleu 3642  eunex 3696  moabex 3708  copsex2t 3733  copsex2g 3734  moop2 3743  mosubopt 3746  hbopab 3754  opelopabf 3765  posn 3794  pofun 3795  frminex 3824  onfr 3882  iunsuc 3925  euuni 3977  reuuni2f 3979  reuuni2 3980  reucl2 3984  reusn 3988  eusvhb 3993  eusv2OLD 3995  eusv2 3996  reusv1lem 3997  reusv1 3998  reusv2lem2 4000  reusv2lem3 4001  reusv2lem4 4002  reusv2 4004  reusv3 4006  reusv6OLD 4009  reusv8OLD 4011  eusvobj1 4012  alxfr 4014  ralxfrd 4015  ralxfr 4017  rabxfrd 4020  reuunixfr 4028  onminsb 4054  onminesb 4055  onminex 4063  tfis 4107  tfis2 4109  tfinds 4111  tfindes 4114  tfinds2 4115  peano5 4141  findes 4148  ralxp 4206  ralxpf 4208  hbrel 4238  hbco 4290  hbcnv 4299  dfdmf 4310  dfrnf 4348  hbrn 4351  hbres 4374  csbima12g 4425  asymref2 4456  intirr 4457  dffun3 4574  dffun6f 4577  dffun6 4578  hbfun 4585  fun11 4619  imadif 4631  funimaexg 4633  isarep1 4635  isarep2 4636  zfrep6 4679  fnopabg 4680  hbfv 4810  csbfv12g 4813  csbfv2g 4815  fv3 4818  tz6.12f 4823  tz6.12-2 4824  tz6.12c 4825  funfv2f 4857  fvopab4gf 4869  fvopab4s 4871  fvopabgf 4875  fvopabnf 4876  fvopab 4878  fvopab2 4879  fvopabs 4880  fvopab5 4881  eqfnfv2f 4895  eufnfv 4896  elrnopabg 4898  fopab2 4927  rnssopab 4929  ffnfv 4932  ffnfvf 4933  fopabco 4936  fopabcos 4937  abrexexlem2 4967  abrexex2g 4971  opabex3 4972  funiunfvf 4977  abrexex2 4981  dff13f 4985  cbvfo 4995  hbiso 5002  isotrALT 5010  csboprg 5045  csbopr12g 5046  csbopr1g 5047  csbopr2g 5048  oprabbid 5055  oprabbidv 5056  cbvoprab1 5058  cbvoprab12 5059  cbvoprab12v 5060  oprabval2gf 5088  oprabval2g 5089  oprabval4g 5093  oprabval4gALT 5094  cbvmpt 5146  cbvmptv 5147  fvmptd 5160  dfopab2 5204  dfoprab3 5205  dfoprab5sf 5209  oprabopabf 5210  oprabopab 5211  foprab2 5214  elrnoprabg 5225  oprabco 5227  1stconst 5233  2ndconst 5234  iunfoprab 5235  fparlem1 5244  fparlem2 5245  hbiota1 5261  hbiota 5262  hbiotad 5263  cbviotaf 5264  cbviota 5265  sb8iota 5266  reiota2df 5283  reiota2f 5284  reiota2 5285  iunon 5291  iinon 5292  onopriun 5295  smores 5303  tfrlem1 5322  tfr3 5338  hbrdg 5348  frsucopab 5366  tz7.48-1 5371  tz7.49OLD 5373  tz7.49 5375  abianfplem 5377  oawordeulem 5439  oarec 5447  eqerlem 5528  ixpf 5619  dom2d 5667  omxpenlem 5712  pw2en 5714  ac6sfilem1 5715  ac6sfilem3 5717  ac6sfi 5718  tskwe 5766  hbriota1 5782  hbriota 5783  hbriotad 5784  cbvriota 5785  csbriotag 5786  riotacl2 5795  riota5f 5798  riota5 5799  riotaxfrd 5801  riotasv2d 5804  riotasv2dOLD 5805  riotasv2s 5806  riotasv2sOLD 5807  riotasv 5808  riotasv3d 5809  riotasv3dOLD 5810  mapxpen 5824  xpmapenlem3 5827  xpmapenlem5 5829  nneneq 5842  isinf 5872  fineqvlem 5873  pssnn 5878  findcard2 5888  unblem2 5897  unblem3 5898  unbnn 5900  fiint 5916  indexfi 5922  iunfi 5927  ordtypelem4 5962  ordtypelem5 5963  ordtypelem6 5964  ordtypelem7 5965  ordtype 5966  sucprcreg 5979  inf0 5988  trcl 6033  r1suc 6047  r1val1 6056  tz9.12lem3 6059  tz9.13g 6062  rankidb 6074  rankid 6084  rankuni2 6102  rankval4 6114  ssralv2 6128  19.21a3con13v 6130  scottex 6150  scott0 6151  scottexs 6152  scott0s 6153  cp 6156  hta 6162  ondomcard 6198  cardmin2 6203  alephon 6219  alephsuc 6220  alephordilem1 6223  omsubsdomlem1 6235  omsubsdomlem2 6236  elomsubsd 6241  infenomsub 6245  aceq1 6248  aceq5lem5 6258  cardaleph 6280  alephfplem2 6294  onacda 6326  axcc2 6361  axcc3 6362  axcc3OLD 6364  domtriomlem 6365  domtriomlemOLD 6366  domtriomOLD 6368  domtriomlemOLDOLD 6369  domtriomOLDOLD 6370  axdc2 6375  axdc3lem2 6377  axdc3lem4 6379  axdc4lem 6381  ac6lem 6395  ac6c4 6397  kmlem14 6424  kmlem15 6425  zorn2lem4 6438  zorn2lem5 6439  axdclem 6445  axdc 6447  brdom3 6451  brdom7disj 6454  brdom6disj 6455  uniimadomf 6462  ondomcardOLD 6498  cardmin 6500  cardprcOLD 6501  alephsucOLD 6503  konigthlem 6504  konigthlemOLD 6506  alephordilem1OLD 6513  cardalephOLD 6520  axrepndlem1 6539  axrepndlem2 6540  axunnd 6543  axpowndlem2 6545  axpowndlem4 6547  axregndlem2 6550  axinfnd 6553  axacndlem4 6557  axacndlem5 6558  zfcndrep 6561  zfcndpow 6563  zfcndinf 6565  zfcndac 6566  suppsrlem 6816  suppsr2 6818  suppsr3 6819  hbneg 7117  subaddi 7126  divmuli 7327  nn1suc 7557  lble 7704  dfuzi 7869  uzindOLD 7875  nn0ind-raph 7883  uzind4s 8082  uzind4s2 8083  nnwof 8089  nnwos 8090  lbzbi 8110  fzrevral 8183  om2uzsuci 8192  seq1lem1 8211  cau3ii 8667  bccl2 8724  hbsum1 8755  hbsum 8756  sumeq2 8757  fsumserzfi 8772  fsum1fi 8779  fsum1slem 8780  fsump1fi 8783  fsump1slem 8784  fsum1p 8791  fsumconst 8810  ser1ser0i 8820  binomlem1 8838  binomlem2 8839  binomlem4 8841  clm4lei 8853  climeu 8872  iserzshft2i 8879  climsupi 8927  caucvglem6 8934  isumvaltfi 8966  isumclim 8969  isumclim2 8972  isumnn0nnai 8981  isummulc1 8985  isummulc1ai 8987  isumcmpii 8988  supcvgOLD 8995  infcvgaux1i 8996  arisumi 9003  fsum0diaglem2 9035  fsum0diag 9036  fsum0diag2 9037  fsum0diag4 9039  divalgb 9437  lubprop 9724  glbprop 9729  tgval3 9896  islp2 10039  cncnplem2 10068  metequiv 10174  iscaunns 10238  fsumcnlem 10285  gafo 10472  gapm 10483  minvecdist 10957  spwpr2 11028  grothprim 11170  fine 11203  inficlALT 11205  hausfillim2 11321  holimf 11322  chcmhi 11738  cnlnadjlem5 12631  adjbdln 12643  rnbra 12667  atom1d 12914  irred 12956  bnj24 13345  bnj34 13356  bnj37 13359  bnj47 13367  bnj48 13370  bnj54 13374  bnj55 13375  bnj58 13376  bnj62 13378  bnj77 13382  bnj79 13384  bnj100 13391  bnj99 13392  bnj112 13397  bnj220 13443  bnj525 13455  bnj853 13716  bnj870 13727  bnj876 13732  bnj912 13751  bnj921 13757  bnj919 13758  bnj1036 13815  bnj1096 13845  bnj1146 13872  bnj1216 13918  bnj1306 13978  bnj1310 13979  bnj1341 13995  bnj1346 14000  bnj1348 14001  bnj1349 14002  bnj1350 14003  bnj1351 14004  bnj1352 14005  bnj1353 14006  bnj1354 14007  bnj1355 14008  bnj1347 14009  bnj1357 14011  bnj1360 14014  bnj1366 14020  bnj1385 14031  bnj1400 14043  bnj1468 14074  bnj1479 14084  bnj1483 14089  bnj1492 14090  bnj1534 14112  bnj1542 14119  bnj65 14131  bnj81 14138  bnj82 14139  bnj86 14142  bnj87 14143  bnj91 14144  bnj92 14145  bnj109 14155  bnj119 14158  bnj121 14160  bnj124 14163  bnj130 14169  bnj154 14174  bnj155 14175  bnj207 14177  bnj571 14218  bnj573 14219  bnj578 14220  bnj605 14221  bnj594 14229  bnj580 14230  bnj607 14233  bnj611 14236  bnj75 14239  bnj873 14246  bnj849 14247  bnj900 14254  bnj894 14256  bnj911 14260  bnj916 14261  bnj958 14273  bnj965 14275  bnj964 14276  bnj981 14285  bnj983 14286  bnj985 14288  bnj1000 14293  bnj1014 14303  bnj1037 14315  bnj1093 14340  bnj1123 14351  bnj1129 14354  bnj1128 14357  bnj1145 14360  bnj1137 14362  bnj1228 14385  bnj1229 14386  bnj1268 14401  bnj1309 14416  bnj1307 14417  bnj1308 14418  bnj1313 14423  bnj1319 14424  bnj1321 14427  bnj1332 14428  bnj1375 14438  bnj1390 14442  bnj1398 14444  bnj1404 14446  bnj1417 14459  bnj1443 14462  bnj1445 14464  bnj1446 14465  bnj1447 14466  bnj1448 14467  bnj1449 14468  bnj1466 14477  bnj1467 14478  bnj1463 14479  bnj1482 14480  bnj1488 14482  bnj1491 14485  bnj1497 14489  bnj1499 14490  bnj1519 14497  bnj1520 14498  bnj1525 14501  bnj1529 14503  bnj1530 14504  hbsum1NEW 14596  hbsumNEW 14597  sumeq2NEW 14598  cbvsumiNEW 14599  untsucf 14676  setinds 14725  setinds2 14727  dfon2lem1 14730  dfon2lem3 14732  frsucopabn 14801  tfisg 14803  wfisg 14809  wfis2g 14813  trpredlem1 14826  trpredtr 14829  trpredmintr 14830  trpred0 14835  trpredrec 14837  frinsg 14841  frins2g 14845  frins2 14846  soseq 14855  wfr3g 14856  frr3g 14880  sltval2 14909  axfelem5 14950  quantriv 15097  imgfldref2 15339  prj1b 15366  prj3 15367  ab2rexexg 15444  ssiingOLD 15457  fopab2g 15480  hbcp 15500  npincppr 15501  repcpwti 15503  cbicplem 15508  unprj 15511  iserzmulc1b 15528  dutos1 15626  tostos 15637  isdir2 15640  hbprod1 15659  hbprod 15660  prodeq2 15661  fprodserzfi 15672  fprod1fi 15675  fprod1slem 15676  fprodp1fi 15680  fprodp1slem 15681  fprod1ib 15686  mgmlion 15693  fincmpzer 15707  fnopabco2b 15730  curgrpact 15731  fprodneg 15737  trooo 15753  cmprtr 15755  ltrooo 15764  cmpltr 15767  cmprltr2 15774  rltrooo 15778  svli2 15840  cmphmp 15896  homcard 15911  intopcoaconlem3 15921  intopcoaconlem3b 15922  intopcoaconb 15923  intopcoaconc 15924  stoig2b 15929  qusp 15932  ttcn2 15939  fgsb 15948  fgsb2 15952  cnfilca 15954  limptlimpr2lem1 15984  bwt2 15999  trhom 16022  grphmlem1 16030  grphmlem2 16031  grphlem3 16032  grphlem5 16034  grphm 16035  cntrsetlem 16052  cnvtr 16069  imonclem 16217  ismonc 16218  cmpmon 16219  iepiclem 16227  isepic 16228  tarval1 16285  tarval2 16320  btmp 16323  isline1 16365  eqeu 16436  subtr 16437  subtr2 16438  cbvcsb 16439  cbvsbcOLD 16440  cbviinvOLD 16443  finminlem 16452  inficlALTOLD 16457  ordtypelem4OLD 16463  ordtypelem5OLD 16464  ordtypelem6OLD 16465  ordtypelem7OLD 16466  ordtypeOLD 16467  omsubsdomlem1OLD 16473  omsubsdomlem2OLD 16474  elomsubsdOLD 16479  infenomsubOLD 16483  hscptsscld 16519  alexsublem3 16524  neibastop1 16603  neibastop2lem1 16604  neibastop2lem2 16605  neibastop2lem3 16606  neibastop2lem4 16607  neibastop3 16609  topmeet 16611  topjoin 16612  limfilcf 16672  sbmoOLD 16739  unirep 16749  cover2 16758  opabex3OLD 16786  cbvoprab2 16793  fnopabco 16796  cbvixp 16808  cbvixpv 16809  hbixp1 16810  abrexex2gOLD 16823  firnfi3 16828  findcard2OLD 16830  ac6gf 16834  indexa 16838  indexdom 16839  indexfiOLD 16840  pofunOLD 16857  frminexOLD 16858  filbcmb 16861  sdclem2 16895  sdc 16896  fdc1 16898  fsumltisumi 16908  fsumleisumi 16911  isumclf 16913  fsumlt1 16916  mettrifi 16932  mettrifi2 16933  oprpiece1res1 16965  oprpiece1res2 16966  cncfres 16980  cnresoprab 17000  cnopropabco 17002  cnoproprabco 17004  cnoprab1 17006  cnoprab2 17007  totbndbnd 17029  prtlem5 17330  pm10.12 17389  19.31vv 17422  pm11.53 17429  aaanv 17430  pm11.57 17431  pm11.58 17432  pm11.59 17433  pm11.71 17439  ax10ext 17449  dvelimfALT2OLD 17451  ax12OLD 17452  pm13.192 17459  2sbc6g 17464  2sbc5g 17465  pm14.12 17470  cla4gftOLD 17491  rcla4tOLD 17492  cbvralcsfOLD 17496  cbvrexcsfOLD 17497  cbvreucsfOLD 17498  cbvrabcsfOLD 17499  compab 17503  cbviotafOLD 17517  cbviotaOLD 17518  smoresOLD 17529  ax172 17576  19.21a3con13vVD 17771  ssralv2VD 17785  riotaoc 17865  glbconx 18036  pmapglbx 18473  pmapglb2x 18476  cdleme26ee 19028  cdleme31so 19048  cdleme31sn 19049  cdleme31sn1 19050  cdleme31se 19051  cdleme31se2 19052  cdleme31sc 19053  cdleme31sn2 19059  cdleme31fv2 19063  cdlemefrs29bpre0 19066  cdlemefrs32fva 19070  cdlemefr29ex 19072  cdlemefs32sn1aw 19084  cdleme43fsv1snlem 19090  cdleme41sn3a 19104  cdleme32fva 19108  cdleme32a 19113  cdleme32d 19116  cdleme32f 19118  cdleme40m 19139  cdleme40nOLD 19140  cdleme40n 19141  cdleme42b 19153  cdlemg1a 19245  cdlemg1ci1 19256  tendopl2 19442  tendoi2 19457  edringplus2 19463

Copyright terms: Public domain