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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2182. (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 1541	. 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  1956  spvw  1989  19.3v  1990  19.8v  1991  spimevw  2003  spimvw  2004  spw  2042  cbvalvw  2044  alcomiw  2051  alcomiwOLD  2052  hbn1w  2054  naev2  2069  sbv  2096  ax12wlem  2134  nf5dv  2150  ax12v  2178  cleljustALT  2365  dvelim  2452  dvelimv  2453  axc16ALT  2494  eujustALT  2573  abeq2  2872  ralrimiv  3107  mpteq12  5161  hashgt23el  14042  bnj1096  32637  bnj1350  32680  bnj1351  32681  bnj1352  32682  bnj1468  32701  bnj1000  32796  bnj1311  32879  bnj1445  32899  bnj1523  32926  umgr2cycllem  32977  umgr2cycl  32978  bj-ax12wlem  34727  bj-cbvalim  34728  bj-cbvexim  34729  bj-cbvexivw  34755  bj-ax12v3  34769  bj-ax12v3ALT  34770  bj-nnfv  34838  bj-abvALT  34994  copsex2b  35214  opelopabbv  35217  brabd  35222  fvineqsnf1  35487  wl-nfalv  35590  mpobi123f  36226  mptbi12f  36230  ax5ALT  36827  dveeq2-o  36853  dveeq1-o  36855  ax12el  36862  ax12a2-o  36870  intimasn  41127  alrim3con13v  42015  ax6e2nd  42040  19.21a3con13vVD  42334  tratrbVD  42343  ssralv2VD  42348  ax6e2ndVD  42390  ax6e2ndALT  42412  stoweidlem35  43439  eu2ndop1stv  44477