Axiom ax-17 1190

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. If we allow the otherwise redundant ax-15 1109 and ax-16 1194, this axiom is logically redundant since it is a metatheorem justified by induction on the number of primitive connectives in wff ph, using ax17eq 1195 and ax17el 1196 together hbn 980, hbal 981, and hbim 983. 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 is effectively a definition of 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 950	. 2 wff A.xph
4	1, 3	wi 3	1 wff (ph -> A.xph)

This axiom is referenced by:  a4b 1191  ax16 1193  dveeq2 1197  19.23adv 1198  ax11a2 1200  equid1 1253  a4w 1255  equvin 1257  albidv 1260  exbidv 1261  19.9v 1266  19.21v 1267  19.21aiv 1268  19.21adv 1270  19.20dv 1271  19.22dv 1272  19.23v 1275  19.23aiv 1277  19.27v 1280  19.28v 1281  19.36v 1282  19.36aiv 1283  19.37v 1285  19.41v 1287  19.42v 1290  cbvalv 1296  cbvexv 1297  cbval2 1298  cbvex2 1299  cbval2v 1300  cbvex2v 1301  cbvald 1302  eeanv 1305  nexdv 1308  cleljust 1310  equsb3lem 1311  equsb3 1312  elsb3 1313  sb7 1322  sb7f 1323  sbid2v 1325  exsb 1332  dvelim 1334  dveeq1 1335  dveel1 1336  dveel2 1337  ax15 1339  ax11el 1341  euf 1361  eubidv 1363  sb8eu 1367  mo 1370  euex 1371  euorv 1376  mo4f 1379  mo4 1380  eu5 1386  immo 1394  moimv 1396  moanim 1404  moanimv 1406  euanv 1409  mopick 1410  moexexv 1416  2mo 1424  2mos 1425  2eu4 1429  2eu6 1431  bm1.1 1439  cleqf 1536  hbel 1542  hbeleq 1543  abeq2 1544  abbidv 1553  clelab 1557  sbabel 1560  ralbidva 1635  rexbidva 1636  ralbidv 1639  rexbidv 1640  2ralbida 1653  2ralbidva 1654  rgen2a 1675  r19.20dva 1685  r19.21aiv 1689  r19.21v 1692  r19.21adv 1694  r19.22dv 1713  r19.12 1716  r19.23aiv 1719  r19.23adv 1722  hbrab 1749  ralcom2 1752  raleq1 1762  rexeq1 1763  reueq1 1764  cbvralf 1772  cbvral 1773  cbvrex 1774  cbvralv 1775  cbvrexv 1776  cbvreuv 1777  rabeq 1784  ceqsalv 1802  ceqsexv 1810  ceqsex2 1811  ceqsex2v 1812  vtocl 1817  vtoclgf 1821  vtoclg 1822  vtocl2gf 1824  vtocl2g 1825  vtoclgaf 1826  vtoclga 1827  cla4gf 1835  cla4gv 1837  cla4egv 1838  rcla4 1844  rcla4e 1845  rcla4v 1846  rcla4ev 1850  eqvincf 1856  ceqsexg 1859  ceqsexgv 1860  elabgt 1867  elabf 1868  elab 1869  elabg 1871  elrab 1877  cbvabv 1881  cbvrab 1882  cbvrabv 1883  mo2icl 1895  moi 1896  reu2 1901  reu6 1903  sbhyp 1911  sbralie 1912  hbsbc1g 1919  hbsbc1 1920  hbsbc1v 1921  hbsbcg 1922  sbccog 1923  sbcco2 1924  sbc5g 1925  sbc6g 1926  sbcieg 1932  elrabsf 1934  elabs2 1935  cbvralsv 1938  cbvrexsv 1939  sbcbidv 1948  sbcel1gv 1951  sbcel2gv 1952  hbsbc1gd 1954  hbsbcgd 1955  sbcralt 1961  sbcralgf 1963  sbcralg 1965  sbcrexg 1966  sbcabel 1967  csbexg 1979  sbcel12g 1982  sbcel1g 1984  sbceq1dig 1985  sbcel2g 1986  sbceq2dig 1987  csbeq2dv 1990  hbcsb1g 1995  hbcsbg 1997  hbcsb1gd 1998  hbcsbgd 1999  csbieb 2001  csbie2t 2004  csbnestglem 2006  csbnest1g 2008  csbidmg 2010  csbco3g 2011  sbcco3g 2012  csbabg 2014  dfss2f 2031  uniiunlem 2103  ne0f 2258  ne0 2259  abn0 2261  hbif 2344  hbpw 2378  eusn 2416  hbuni 2477  eluniab 2481  hbint 2511  elintab 2512  ssintab 2518  intab 2528  cbviunv 2558  ssiun2s 2562  iunrab 2564  iunid 2571  iununi 2584  sbcbrg 2630  sbcbr12g 2631  sbcbr1g 2632  sbcbr2g 2633  opabbid 2637  opabbidv 2638  cbvopab 2640  cbvopabv 2641  cbvopab1 2642  cbvopab1s 2643  cbvopab1v 2644  csbopabg 2646  axrep1 2662  axrep2 2663  axrep3 2664  axrep4 2665  axrep5 2666  zfrepclf 2667  zfrep3cl 2668  axsep 2670  zfnuleu 2675  moabex 2734  copsex2g 2760  moop2 2766  mosubopt 2767  opabid 2772  hbopab 2774  opabsb 2777  dfid3 2799  euuni 2844  reuuni2f 2846  reuuni2 2847  reucl 2848  reucl2 2851  reusn 2855  alxfr 2859  ralxfrd 2860  ralxfr 2862  rabxfr 2865  reuunixfr 2869  onfr 2949  onminsb 2972  onminesb 2973  onminex 2983  tfis 3090  tfis2 3092  peano5 3116  findes 3123  tfinds 3124  tfindes 3127  tfinds2 3128  hbxp 3167  ralxp 3180  ralxpf 3182  hbrel 3207  hbco 3244  hbcnv 3252  dfdmf 3263  dfrnf 3304  hbrn 3307  dmcosseq 3316  hbres 3321  hbima 3362  csbima12g 3364  cnvopab 3394  dffun3 3468  dffunmof 3471  dffunmo 3472  hbfun 3477  funeu 3478  dffun7 3481  fun11 3502  imadif 3514  funimaexg 3515  isarep1 3517  isarep2 3518  fneu 3532  zfrep6 3554  fnopabg 3555  hbfv 3668  fv3 3672  tz6.12f 3677  tz6.12-2 3678  tz6.12c 3679  csbfv12g 3681  csbfv2g 3682  funfv2f 3711  fvopab4gf 3720  fvopab4s 3722  fvopabgf 3726  fvopabnf 3727  fvopab 3729  fvopab2 3730  fvopabs 3731  fvopab5 3732  eqfnfvf 3737  elrnopabg 3739  fopab2 3762  rnssopab 3764  ffnfv 3767  ffnfvf 3768  fopabco 3771  fopabcos 3772  fopabsn 3779  abrexexlem2 3798  funiunfvf 3809  abrexex2 3810  f1fvf 3814  cbvfo 3824  hbiso 3831  isotrALT 3837  iunon 3848  iinon 3849  tfrlem1 3850  tfr3 3865  hbrdg 3875  frsucopab 3893  tz7.48-1 3895  tz7.49 3898  abianfplem 3900  csboprg 3925  csbopr12g 3926  csbopr1g 3927  csbopr2g 3928  oprabbid 3934  oprabbidv 3935  cbvoprab12 3937  cbvoprab12v 3938  oprabval2gf 3965  oprabval2g 3966  oprabval4g 3970  2ndconst 4035  dfopab2 4051  dfoprab3 4052  dfoprab5 4053  foprab2 4057  elrnoprabg 4062  oawordeulem 4126  oarec 4134  eqerlem 4208  ixpf 4294  dom2d 4339  pw2en 4380  mapxpen 4427  xpmapenlem3 4430  xpmapenlem5 4432  nneneq 4444  pssnn 4465  unblem2 4470  unblem3 4471  unbnn 4473  fiint 4486  iunfi 4495  sucprcreg 4524  inf0 4530  trcl 4569  r1suc 4576  r1val1 4582  tz9.12lem3 4585  tz9.13g 4588  rankid 4596  rankuni2 4614  rankval4 4626  scottex 4640  scott0 4641  scottexs 4642  scott0s 4643  cp 4646  hta 4652  aceq1 4653  aceq5lem5 4663  ac6lem 4678  kmlem14 4702  kmlem15 4703  zorn2lem4 4715  zorn2lem5 4716  brdom3 4725  brdom7disj 4728  brdom6disj 4729  uniimadomf 4735  ondomcard 4780  cardmin 4783  cardprc 4784  alephon 4788  alephsuc 4789  alephordlem1 4795  cardaleph 4808  alephfplem2 4820  axrepndlem1 4867  axrepndlem2 4868  axunndlem1 4870  axunnd 4871  axpowndlem2 4873  axpowndlem4 4875  axregndlem2 4878  axinfnd 4881  axacndlem4 4885  axacndlem5 4886  zfcndrep 4889  zfcndpow 4891  zfcndinf 4893  zfcndac 4894  suppsrlem 5144  suppsr2 5146  suppsr3 5147  hbneg 5285  csbnegg 5287  nn1suc 5838  lble 5945  dfuz 6101  uzindOLD 6107  nn0ind-raph 6113  om2uzsuc 6184  seq1lem1 6197  uzind4s 6335  uzind4s2 6336  nnwof 6342  nnwos 6343  fzrevralt 6402  cau3i 6802  bccl2t 6860  hbsum1 6872  hbsum 6873  sumeq2 6874  fsumserzf 6889  fsum1f 6896  fsum1slem 6897  fsump1f 6900  fsump1slem 6901  fsum1p 6908  fsumconst 6927  ser1ser0 6937  binomlem1 6955  binomlem2 6956  binomlem4 6958  clm4le 6970  climeu 6988  iserzshft2 6995  climsup 7042  caucvglem6 7049  isumvaltf 7080  isumclimt 7083  isumclim2t 7085  isumnn0nna 7094  isummulc1 7098  isummulc1a 7100  isumcmpi 7101  infcvgaux1 7105  fnsmnt 7112  fsum0diaglem2 7143  fsum0diag 7144  fsum0diag2 7145  fsum0diag4 7147  tgval3t 7518  islp2 7636  cncnplem2 7662  fsumcnlem 7871  minvecdist 8451  grothprim 8635  cbvrexf 8698  fine 8707  cmphmp 8759  qusp 8780  fgsb 8794  fgsb2 8799  cnfilca 8801  cnvtr 8832  imonclem 8933  ismonc 8934  cmpmon 8935  chcmh 9264  cnlnadjlem5 10133  adjbdlnt 10145  rnbra 10167  atom1d 10402  irredt 10444

Copyright terms: Public domain