Axiom ax-5 1945

Description: Axiom of Distinctness. This axiom quantifies 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.

(See comments in ax5ALT 40155 about the logical redundancy of ax-5 1945 in the presence of our obsolete axioms.)

This axiom essentially says that if 𝑥 does not occur in 𝜑, i.e. 𝜑 does not depend on 𝑥 in any way, then we can add the quantifier ∀𝑥 to 𝜑 with no further assumptions. By sp 2223, we can also remove the quantifier (unconditionally).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2223. (Contributed by NM, 10-Jan-1993.)

Assertion

Ref	Expression
ax-5	⊢ (𝜑 → ∀𝑥𝜑)

Distinct variable group:   𝜑,𝑥

Detailed syntax breakdown of Axiom ax-5

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wal 1568	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is used by:  ax5d  1946  ax5e  1947  ax5ea  1948  alimdv  1951  eximdv  1952  albidv  1955  exbidv  1956  alrimiv  1962  alrimdv  1964  nexdv  1971  stdpc5v  1973  19.23v  1977  19.37imv  1982  spvw  2016  19.3v  2017  19.8v  2018  spimevw  2020  spimvw  2021  spw  2069  cbvalvw  2071  alcomimw  2078  hbn1w  2083  naev2  2098  sbv  2127  ax12wlem  2171  nf5dv  2188  ax12v  2217  cleljustALT  2396  dvelim  2483  dvelimv  2484  axc16ALT  2521  eujustALT  2600  ralrimiv  3157  mpteq12  5196  hashgt23el  14593  umgr2cycllem  30773  umgr2cycl  30774  bnj1096  35480  bnj1350  35522  bnj1351  35523  bnj1352  35524  bnj1468  35543  bnj1000  35638  bnj1311  35721  bnj1445  35741  bnj1523  35768  srepdf  36086  bj-spvw  37711  bj-spvew  37712  bj-alextruim  37713  bj-cbvalvv  37715  bj-ax12wlem  37721  bj-cbvexivw  37749  bj-ax12v3  37764  bj-ax12v3ALT  37765  bj-nnfv  37847  bj-nnfbd  37848  bj-nnf-cbvaliv  37855  bj-abvALT  37996  copsex2b  38252  opelopabbv  38255  brabd  38260  fvineqsnf1  38524  wl-nfalv  38648  findcard4  38823  mpobi123f  39285  mptbi12f  39289  ecqmap  39572  ax5ALT  40155  dveeq2-o  40181  dveeq1-o  40183  ax12el  40190  ax12a2-o  40198  intimasn  44847  alrim3con13v  45705  ax6e2nd  45730  19.21a3con13vVD  46023  tratrbVD  46032  ssralv2VD  46037  ax6e2ndVD  46079  ax6e2ndALT  46101  stoweidlem35  47248  eu2ndop1stv  48398