Axiom ax-5 1918

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

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

This axiom is referenced by:  ax5d  1919  ax5e  1920  ax5ea  1921  alimdv  1924  eximdv  1925  albidv  1928  exbidv  1929  alrimiv  1935  alrimdv  1937  nexdv  1944  stdpc5v  1946  19.23v  1950  19.37imv  1955  spvw  1989  19.3v  1990  19.8v  1991  spimevw  1993  spimvw  1994  spw  2042  cbvalvw  2044  alcomimw  2051  hbn1w  2056  naev2  2071  sbv  2100  ax12wlem  2145  nf5dv  2161  ax12v  2192  cleljustALT  2374  dvelim  2461  dvelimv  2462  axc16ALT  2499  eujustALT  2578  ralrimiv  3132  mpteq12  5162  hashgt23el  14381  bnj1096  34978  bnj1350  35020  bnj1351  35021  bnj1352  35022  bnj1468  35041  bnj1000  35136  bnj1311  35219  bnj1445  35239  bnj1523  35266  umgr2cycllem  35381  umgr2cycl  35382  bj-spvw  36988  bj-spvew  36989  bj-alextruim  36990  bj-cbvalvv  36992  bj-ax12wlem  36998  bj-cbvexivw  37026  bj-ax12v3  37041  bj-ax12v3ALT  37042  bj-nnfv  37124  bj-nnfbd  37125  bj-nnf-cbvaliv  37132  bj-abvALT  37273  copsex2b  37513  opelopabbv  37516  brabd  37521  fvineqsnf1  37785  wl-nfalv  37909  mpobi123f  38542  mptbi12f  38546  ecqmap  38829  ax5ALT  39412  dveeq2-o  39438  dveeq1-o  39440  ax12el  39447  ax12a2-o  39455  intimasn  44114  alrim3con13v  44990  ax6e2nd  45015  19.21a3con13vVD  45308  tratrbVD  45317  ssralv2VD  45322  ax6e2ndVD  45364  ax6e2ndALT  45386  stoweidlem35  46490  eu2ndop1stv  47600