MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-4 Unicode version

Axiom ax-4 1692
Description: Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all  x, it is true for any specific  x (that would typically occur as a free variable in the wff substituted for  ph). (A free variable is one that does not occur in the scope of a quantifier:  x and  y are both free in  x  =  y, but only  x is free in  A. y x  =  y.) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1692 through ax-7 1535 plus rule ax-gen 1536). Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77).

Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1536. Conditional forms of the converse are given by ax-12 1633, ax-15 2102, ax-16 1926, and ax-17 1628.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from  x for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1896.

An interesting alternate axiomatization uses ax467 1752 and ax-5o 1694 in place of ax-4 1692, ax-5 1533, ax-6 1534, and ax-7 1535.

This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1691. (We replaced the older ax-5o 1694 and ax-6o 1697 with newer versions ax-5 1533 and ax-6 1534 in order to prove this redundancy.) (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-4  |-  ( A. x ph  ->  ph )

Detailed syntax breakdown of Axiom ax-4
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
31, 2wal 1532 . 2  wff  A. x ph
43, 1wi 6 1  wff  ( A. x ph  ->  ph )
Colors of variables: wff set class
This axiom is referenced by:  ax5o  1693  ax5  1695  ax6o  1696  ax6  1698  a4i  1699  a4s  1700  a4sd  1701  nfr  1702  hba1  1718  ax46  1746  ax67to6  1750  ax467  1752  19.8a  1758  19.3  1760  19.12  1766  19.21t  1770  19.21bi  1774  19.38  1791  hbim1  1810  ax9o  1814  hbae  1840  hbae-o  1841  equsalh  1851  a4imt  1866  equveli  1880  ax12  1881  sb2  1888  ax11  1941  ax11b  1942  dfsb2  1947  nfsb4t  1972  sb56  1991  sb6  1992  a16gb  2002  sbal1  2086  ax11indalem  2110  ax11inda2ALT  2111  mo  2135  mopick  2175  2eu1  2193  nfcr  2377  ra4  2565  ceqex  2835  abidnf  2871  mob2  2882  csbie2t  3053  sbcnestgf  3056  mpteq12f  3993  axrep2  4030  axnulALT  4044  dtru  4095  copsex2t  4146  ssopab2  4183  eusv1  4419  alxfr  4438  dffv2  5444  iota1  6157  fiint  7018  isf32lem9  7871  nd3  8091  axrepnd  8096  axpowndlem2  8100  axacndlem4  8112  ex-natded9.26-2  20665  frmin  23410  wfrlem5  23428  frrlem5  23453  imonclem  24979  prtlem14  25908  setindtr  26283  pm11.57  26754  pm11.59  26756  ax4567to6  26770  ax4567to7  26771  ax10ext  26772  iotain  26784  pm14.123b  26793  eubi  26803  compneOLD  26810  ssralv2  26987  19.41rg  27009  hbexg  27015  ssralv2VD  27332  19.41rgVD  27368  hbimpgVD  27370  hbexgVD  27372  vk15.4jVD  27380  bnj1294  27539  bnj570  27626  bnj953  27660  bnj1204  27731
  Copyright terms: Public domain W3C validator