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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2191. (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  2186  cleljustALT  2369  dvelim  2456  dvelimv  2457  axc16ALT  2494  eujustALT  2573  ralrimiv  3129  mpteq12  5174  hashgt23el  14383  bnj1096  34922  bnj1350  34964  bnj1351  34965  bnj1352  34966  bnj1468  34985  bnj1000  35080  bnj1311  35163  bnj1445  35183  bnj1523  35210  umgr2cycllem  35319  umgr2cycl  35320  bj-spvw  36926  bj-spvew  36927  bj-alextruim  36928  bj-cbvalvv  36930  bj-ax12wlem  36936  bj-cbvexivw  36964  bj-ax12v3  36979  bj-ax12v3ALT  36980  bj-nnfv  37062  bj-nnfbd  37063  bj-nnf-cbvaliv  37070  bj-abvALT  37211  copsex2b  37451  opelopabbv  37454  brabd  37459  fvineqsnf1  37723  wl-nfalv  37847  mpobi123f  38480  mptbi12f  38484  ecqmap  38767  ax5ALT  39350  dveeq2-o  39376  dveeq1-o  39378  ax12el  39385  ax12a2-o  39393  intimasn  44081  alrim3con13v  44957  ax6e2nd  44982  19.21a3con13vVD  45275  tratrbVD  45284  ssralv2VD  45289  ax6e2ndVD  45331  ax6e2ndALT  45353  stoweidlem35  46460  eu2ndop1stv  47564