Axiom ax-17 925

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 ax-15 806 (not otherwise used in our development), this axiom is logically redundant since it is a metatheorem justified by induction on the number of primitive connectives in wff ph, using ax17eq 923 and ax17el 924 together hbne 699, hbal 700, and hbim 702. 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(s):   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 672	. 2 wff A.xph
4	1, 3	wi 2	1 wff (ph -> A.xph)

This axiom is referenced by:  a4b 927  a4w 929  eqvin.l2 931  bialdv 935  biexdv 936  19.9rv 941  19.21v 942  19.21aiv 943  19.21adv 945  19.20dv 946  19.22dv 947  19.23v 950  19.23aiv 952  19.23adv 954  19.27v 956  19.28v 957  19.36v 958  19.36aiv 959  19.37v 961  19.41v 963  19.42v 966  cbvalv 972  cbvexv 973  cbval2 974  cbvex2 975  cbvex2v 976  cbvald 977  eeanv 980  nexdv 983  cleljust 985  sb7 991  sbid2v 993  ddelim 1000  ddeeq1 1001  ddeeq2 1002  ddeel1 1003  ddeel2 1004  euf 1011  bieudv 1013  sb8eu 1017  mo 1020  euex 1021  mo4f 1028  mo4 1029  eu5 1035  immo 1043  moimv 1044  moanim 1051  moanimv 1052  mopick 1054  moexexv 1059  2eu4 1070  bm1.1 1088  cleqf 1167  hbel 1172  hbeleq 1173  cleqab 1174  biabdv 1183  clelab 1187  sbabel 1189  biraldva 1215  birexdva 1216  biraldv 1219  birexdv 1220  bi2ralda 1232  bi2raldva 1233  rgen2 1248  r19.20dva 1256  r19.21aiv 1259  r19.21adv 1262  r19.22dv 1278  r19.12 1281  r19.23aiv 1284  hbrab 1311  ralcom2 1314  raleq 1324  rexeq 1325  reueq 1326  cbvralf 1330  cbvral 1331  cbvrex 1332  cbvralv 1333  cbvrexv 1334  cbvreuv 1335  reu2 1338  reu4 1340  rabeq 1346  ceqsalv 1364  ceqsexv 1371  vtocl 1378  vtoclgf 1382  vtoclg 1383  vtocl2gf 1385  vtocl2g 1386  cla4gf 1394  cla4gv 1396  cla4egv 1397  eqvincf 1408  ceqsexg 1411  ceqsexgv 1412  elabf 1414  elab 1415  elabg 1417  elrab 1422  cbvabv 1424  cbvrab 1425  cbvrabv 1426  mo2icl 1434  vsbcint 1438  sbralie 1439  hbsbcg 1445  hbsbc 1446  hbsbcv 1447  sbcco 1448  sbcco2 1449  sbc5g 1450  sbc6g 1451  elrabsf 1456  elabs2 1457  sbcel1 1466  sbcel2 1467  axrep 1473  axrep2 1474  zfrep2 1475  zfrep3 1476  zfrepclf 1477  zfrep3cl 1478  dfss2f 1499  n0f 1713  n0 1714  abn0 1715  hbpw 1804  moabex 1868  copsex2g 1903  moop2 1910  mosubop 1911  eusn 1913  hbuni 1925  eluniab 1926  euuni 1954  reuuni2 1956  reucl 1957  hbint 1975  elintab 1976  ssiun2s 2020  iunrab 2022  iununi 2037  opabid 2099  biopabd 2101  biopabdv 2102  cbvopab 2104  cbvopabv 2105  cbvopab1 2106  cbvopab1s 2107  hbopab 2111  opabsb 2114  opelopabg 2115  onfr 2237  tfis 2245  tfis2 2247  onminsb 2264  onminesb 2265  onminex 2275  peano5 2394  findes 2400  tfinds 2401  tfindes 2404  tfinds2 2405  hbxp 2444  ralxp 2456  hbrel 2478  hbco 2508  hbcnv 2516  dfdmf 2526  dfrnf 2561  hbrn 2564  dmcosseq 2572  hbres 2577  hbima 2609  cnvopab 2632  dffun3 2675  dffunmof 2678  dffunmo 2679  hbfun 2684  funeu 2685  dffun7 2688  imadif 2714  funimaexg 2715  fneu 2728  zfrep6 2744  fnopabg 2745  hbfv 2837  fv3 2839  tz6.12f 2844  tz6.12-2 2845  tz6.12c 2846  fvopabgf 2874  fvopabnf 2875  fvopab 2877  fvopab2 2878  cleqfvf 2881  elrnopab 2884  fopab2 2891  ffnfv 2892  abrexexlem2 2911  abrexex2 2915  f1fvf 2917  cbvfo 2923  hbiso 2930  isotrALT 2936  iunon 2947  iinon 2948  tfrlem1 2949  tfr3 2964  hbrdg 2974  frsucopab 2992  tz7.48-1 2994  tz7.49 2997  abianfplem 2999  bioprabd 3025  bioprabdv 3026  cbvoprab12 3028  cbvoprab12v 3029  oprabval4g 3053  elrnoprab 3054  oawordeulem 3156  dom2d 3307  pw2en 3348  mapxpen 3390  xpmapenlem3 3393  xpmapenlem5 3395  nneneq 3408  pssnn 3428  unblem2 3432  unblem3 3433  unbnn 3435  fiint 3445  sucprcreg 3451  inf0 3457  trcl 3489  r1suc 3496  r1val1 3502  tz9.12lem3 3505  tz9.13g 3508  rankid 3516  rankuni 3533  ranklon 3540  scottex 3541  scott0 3542  scottexs 3543  scott0s 3544  cp 3547  aceq1 3552  aceq5lem5 3562  ac6lem 3575  kmlem14 3593  kmlem15 3594  zornlem4 3606  zornlem5 3607  hta 3619  ondomcard 3663  cardmin 3666  cardprc 3667  alephon 3671  alephsuc 3672  alephordlem1 3677  cardaleph 3690  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem4 3746  axregndlem2 3749  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  zfcndrep 3760  zfcndpow 3762  zfcndinf 3764  zfcndac 3765  suppsrlem 4015  suppsr2 4017  suppsr3 4018  nn1suc 4435  uzind 4603  nnwof 4609  nnwos 4610  nn0ind 4612  om2uzsuc 4652  seqlem1 4662  chcmh 5148  atom1d 5750

metamath.org