Axiom ax-5 1910

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

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

This axiom is referenced by:  ax5d  1911  ax5e  1912  ax5ea  1913  alimdv  1916  eximdv  1917  albidv  1920  exbidv  1921  alrimiv  1927  alrimdv  1929  nexdv  1936  stdpc5v  1938  19.23v  1942  19.37imv  1947  spvw  1981  19.3v  1982  19.8v  1983  spimevw  1985  spimvw  1986  spw  2034  cbvalvw  2036  alcomimw  2043  hbn1w  2047  naev2  2062  sbv  2089  ax12wlem  2133  nf5dv  2149  ax12v  2179  cleljustALT  2362  dvelim  2449  dvelimv  2450  axc16ALT  2487  eujustALT  2565  eqabbOLD  2868  ralrimiv  3124  mpteq12  5195  hashgt23el  14389  bnj1096  34772  bnj1350  34815  bnj1351  34816  bnj1352  34817  bnj1468  34836  bnj1000  34931  bnj1311  35014  bnj1445  35034  bnj1523  35061  umgr2cycllem  35127  umgr2cycl  35128  bj-ax12wlem  36632  bj-cbvalim  36633  bj-cbvexim  36634  bj-cbvexivw  36660  bj-ax12v3  36673  bj-ax12v3ALT  36674  bj-nnfv  36742  bj-abvALT  36895  copsex2b  37128  opelopabbv  37131  brabd  37136  fvineqsnf1  37398  wl-nfalv  37513  mpobi123f  38156  mptbi12f  38160  ax5ALT  38900  dveeq2-o  38926  dveeq1-o  38928  ax12el  38935  ax12a2-o  38943  intimasn  43646  alrim3con13v  44523  ax6e2nd  44548  19.21a3con13vVD  44841  tratrbVD  44850  ssralv2VD  44855  ax6e2ndVD  44897  ax6e2ndALT  44919  stoweidlem35  46033  eu2ndop1stv  47126