Axiom ax-5 1912

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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2189. (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  1913  ax5e  1914  ax5ea  1915  alimdv  1918  eximdv  1919  albidv  1922  exbidv  1923  alrimiv  1929  alrimdv  1931  nexdv  1938  stdpc5v  1940  19.23v  1944  19.37imv  1949  spvw  1983  19.3v  1984  19.8v  1985  spimevw  1987  spimvw  1988  spw  2036  cbvalvw  2038  alcomimw  2045  hbn1w  2050  naev2  2065  sbv  2094  ax12wlem  2138  nf5dv  2154  ax12v  2184  cleljustALT  2367  dvelim  2454  dvelimv  2455  axc16ALT  2492  eujustALT  2571  ralrimiv  3126  mpteq12  5185  hashgt23el  14349  bnj1096  34917  bnj1350  34960  bnj1351  34961  bnj1352  34962  bnj1468  34981  bnj1000  35076  bnj1311  35159  bnj1445  35179  bnj1523  35206  umgr2cycllem  35313  umgr2cycl  35314  bj-ax12wlem  36817  bj-cbvalim  36818  bj-cbvexim  36819  bj-cbvexivw  36846  bj-ax12v3  36859  bj-ax12v3ALT  36860  bj-nnfv  36928  bj-abvALT  37081  copsex2b  37314  opelopabbv  37317  brabd  37322  fvineqsnf1  37584  wl-nfalv  37699  mpobi123f  38332  mptbi12f  38336  ecqmap  38619  ax5ALT  39202  dveeq2-o  39228  dveeq1-o  39230  ax12el  39237  ax12a2-o  39245  intimasn  43935  alrim3con13v  44811  ax6e2nd  44836  19.21a3con13vVD  45129  tratrbVD  45138  ssralv2VD  45143  ax6e2ndVD  45185  ax6e2ndALT  45207  stoweidlem35  46316  eu2ndop1stv  47408