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 39341 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 2190, we can also remove the quantifier (unconditionally).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2190. (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  2185  cleljustALT  2367  dvelim  2454  dvelimv  2455  axc16ALT  2492  eujustALT  2571  ralrimiv  3126  mpteq12  5162  hashgt23el  14375  bnj1096  34913  bnj1350  34955  bnj1351  34956  bnj1352  34957  bnj1468  34976  bnj1000  35071  bnj1311  35154  bnj1445  35174  bnj1523  35201  umgr2cycllem  35310  umgr2cycl  35311  bj-spvw  36917  bj-spvew  36918  bj-alextruim  36919  bj-cbvalvv  36921  bj-ax12wlem  36927  bj-cbvexivw  36955  bj-ax12v3  36970  bj-ax12v3ALT  36971  bj-nnfv  37053  bj-nnfbd  37054  bj-nnf-cbvaliv  37061  bj-abvALT  37202  copsex2b  37442  opelopabbv  37445  brabd  37450  fvineqsnf1  37714  wl-nfalv  37838  mpobi123f  38471  mptbi12f  38475  ecqmap  38758  ax5ALT  39341  dveeq2-o  39367  dveeq1-o  39369  ax12el  39376  ax12a2-o  39384  intimasn  44072  alrim3con13v  44948  ax6e2nd  44973  19.21a3con13vVD  45266  tratrbVD  45275  ssralv2VD  45280  ax6e2ndVD  45322  ax6e2ndALT  45344  stoweidlem35  46451  eu2ndop1stv  47561