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 39235 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  3128  mpteq12  5187  hashgt23el  14351  bnj1096  34940  bnj1350  34983  bnj1351  34984  bnj1352  34985  bnj1468  35004  bnj1000  35099  bnj1311  35182  bnj1445  35202  bnj1523  35229  umgr2cycllem  35336  umgr2cycl  35337  bj-ax12wlem  36846  bj-cbvalim  36847  bj-cbvexim  36848  bj-cbvexivw  36875  bj-ax12v3  36888  bj-ax12v3ALT  36889  bj-nnfv  36957  bj-abvALT  37110  bj-cbvexvv  37277  copsex2b  37347  opelopabbv  37350  brabd  37355  fvineqsnf1  37617  wl-nfalv  37732  mpobi123f  38365  mptbi12f  38369  ecqmap  38652  ax5ALT  39235  dveeq2-o  39261  dveeq1-o  39263  ax12el  39270  ax12a2-o  39278  intimasn  43965  alrim3con13v  44841  ax6e2nd  44866  19.21a3con13vVD  45159  tratrbVD  45168  ssralv2VD  45173  ax6e2ndVD  45215  ax6e2ndALT  45237  stoweidlem35  46346  eu2ndop1stv  47438