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 37715 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  5239  hashgt23el  14380  bnj1096  33731  bnj1350  33774  bnj1351  33775  bnj1352  33776  bnj1468  33795  bnj1000  33890  bnj1311  33973  bnj1445  33993  bnj1523  34020  umgr2cycllem  34069  umgr2cycl  34070  bj-ax12wlem  35459  bj-cbvalim  35460  bj-cbvexim  35461  bj-cbvexivw  35487  bj-ax12v3  35501  bj-ax12v3ALT  35502  bj-nnfv  35570  bj-abvALT  35725  copsex2b  35959  opelopabbv  35962  brabd  35967  fvineqsnf1  36229  wl-nfalv  36332  mpobi123f  36968  mptbi12f  36972  ax5ALT  37715  dveeq2-o  37741  dveeq1-o  37743  ax12el  37750  ax12a2-o  37758  intimasn  42341  alrim3con13v  43227  ax6e2nd  43252  19.21a3con13vVD  43546  tratrbVD  43555  ssralv2VD  43560  ax6e2ndVD  43602  ax6e2ndALT  43624  stoweidlem35  44686  eu2ndop1stv  45768