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 39344 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  14348  bnj1096  34931  bnj1350  34973  bnj1351  34974  bnj1352  34975  bnj1468  34994  bnj1000  35089  bnj1311  35172  bnj1445  35192  bnj1523  35219  umgr2cycllem  35328  umgr2cycl  35329  bj-spvw  36927  bj-spvew  36928  bj-alextruim  36929  bj-cbvalvv  36931  bj-ax12wlem  36937  bj-cbvexivw  36965  bj-ax12v3  36980  bj-ax12v3ALT  36981  bj-nnfv  37063  bj-nnfbd  37064  bj-nnf-cbvaliv  37071  bj-abvALT  37212  copsex2b  37452  opelopabbv  37455  brabd  37460  fvineqsnf1  37722  wl-nfalv  37841  mpobi123f  38474  mptbi12f  38478  ecqmap  38761  ax5ALT  39344  dveeq2-o  39370  dveeq1-o  39372  ax12el  39379  ax12a2-o  39387  intimasn  44087  alrim3con13v  44963  ax6e2nd  44988  19.21a3con13vVD  45281  tratrbVD  45290  ssralv2VD  45295  ax6e2ndVD  45337  ax6e2ndALT  45359  stoweidlem35  46467  eu2ndop1stv  47559