Axiom ax-5 1914

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 37777 about the logical redundancy of ax-5 1914 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 2177, we can also remove the quantifier (unconditionally).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2177. (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 1540	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  1915  ax5e  1916  ax5ea  1917  alimdv  1920  eximdv  1921  albidv  1924  exbidv  1925  alrimiv  1931  alrimdv  1933  nexdv  1940  stdpc5v  1942  19.23v  1946  19.37imv  1952  spvw  1985  19.3v  1986  19.8v  1987  spimevw  1999  spimvw  2000  spw  2038  cbvalvw  2040  alcomiw  2047  hbn1w  2050  naev2  2065  sbv  2092  ax12wlem  2129  nf5dv  2145  ax12v  2173  cleljustALT  2362  dvelim  2451  dvelimv  2452  axc16ALT  2489  eujustALT  2567  eqabbOLD  2875  ralrimiv  3146  mpteq12  5241  hashgt23el  14384  bnj1096  33793  bnj1350  33836  bnj1351  33837  bnj1352  33838  bnj1468  33857  bnj1000  33952  bnj1311  34035  bnj1445  34055  bnj1523  34082  umgr2cycllem  34131  umgr2cycl  34132  bj-ax12wlem  35521  bj-cbvalim  35522  bj-cbvexim  35523  bj-cbvexivw  35549  bj-ax12v3  35563  bj-ax12v3ALT  35564  bj-nnfv  35632  bj-abvALT  35787  copsex2b  36021  opelopabbv  36024  brabd  36029  fvineqsnf1  36291  wl-nfalv  36394  mpobi123f  37030  mptbi12f  37034  ax5ALT  37777  dveeq2-o  37803  dveeq1-o  37805  ax12el  37812  ax12a2-o  37820  intimasn  42408  alrim3con13v  43294  ax6e2nd  43319  19.21a3con13vVD  43613  tratrbVD  43622  ssralv2VD  43627  ax6e2ndVD  43669  ax6e2ndALT  43691  stoweidlem35  44751  eu2ndop1stv  45833