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 , it is true for any specific (that would typically occur as a free variable in the wff substituted for ). (A free variable is one that does not occur in the scope of a quantifier: and are both free in , but only is free in .) 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 2105, ax-16 1927, and ax-17 1628. Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from 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 1897. 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

Detailed syntax breakdown of Axiom ax-4
StepHypRef Expression
1 wph . . 3
2 vx . . 3
31, 2wal 1532 . 2
43, 1wi 6 1
 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  1841  hbae-o  1842  equsalh  1852  a4imt  1867  equveli  1881  ax12  1882  sb2  1889  ax11  1942  ax11b  1943  dfsb2  1948  nfsb4t  1973  sb56  1992  sb6  1993  a16gb  2003  sbal1  2089  ax11indalem  2113  ax11inda2ALT  2114  mo  2138  mopick  2178  2eu1  2196  nfcr  2384  ra4  2576  ceqex  2866  abidnf  2902  mob2  2913  csbie2t  3086  sbcnestgf  3089  mpteq12f  4056  axrep2  4093  axnulALT  4107  dtru  4159  copsex2t  4211  ssopab2  4248  eusv1  4486  alxfr  4505  dffv2  5512  iota1  6225  fiint  7087  isf32lem9  7941  nd3  8165  axrepnd  8170  axpowndlem2  8174  axacndlem4  8186  ex-natded9.26-2  20781  frmin  23597  wfrlem5  23615  frrlem5  23640  imonclem  25166  prtlem14  26095  setindtr  26470  pm11.57  26941  pm11.59  26943  ax4567to6  26957  ax4567to7  26958  ax10ext  26959  iotain  26971  pm14.123b  26980  eubi  26990  compneOLD  26997  ssralv2  27331  19.41rg  27353  hbexg  27359  ssralv2VD  27676  19.41rgVD  27712  hbimpgVD  27714  hbexgVD  27716  vk15.4jVD  27724  bnj1294  27883  bnj570  27970  bnj953  28004  bnj1204  28075
 Copyright terms: Public domain W3C validator