Axiom ax-5 1943

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

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

This axiom is used by:  ax5d  1944  ax5e  1945  ax5ea  1946  alimdv  1949  eximdv  1950  albidv  1953  exbidv  1954  alrimiv  1960  alrimdv  1962  nexdv  1969  stdpc5v  1971  19.23v  1975  19.37imv  1980  spvw  2014  19.3v  2015  19.8v  2016  spimevw  2018  spimvw  2019  spw  2067  cbvalvw  2069  alcomimw  2076  hbn1w  2081  naev2  2096  sbv  2125  ax12wlem  2169  nf5dv  2185  ax12v  2214  cleljustALT  2393  dvelim  2480  dvelimv  2481  axc16ALT  2518  eujustALT  2597  ralrimiv  3153  mpteq12  5192  hashgt23el  14536  umgr2cycllem  30679  umgr2cycl  30680  bnj1096  35347  bnj1350  35389  bnj1351  35390  bnj1352  35391  bnj1468  35410  bnj1000  35505  bnj1311  35588  bnj1445  35608  bnj1523  35635  bj-spvw  37456  bj-spvew  37457  bj-alextruim  37458  bj-cbvalvv  37460  bj-ax12wlem  37466  bj-cbvexivw  37494  bj-ax12v3  37509  bj-ax12v3ALT  37510  bj-nnfv  37592  bj-nnfbd  37593  bj-nnf-cbvaliv  37600  bj-abvALT  37741  copsex2b  37981  opelopabbv  37984  brabd  37989  fvineqsnf1  38253  wl-nfalv  38377  findcard4  38552  mpobi123f  39014  mptbi12f  39018  ecqmap  39301  ax5ALT  39884  dveeq2-o  39910  dveeq1-o  39912  ax12el  39919  ax12a2-o  39927  intimasn  44601  alrim3con13v  45460  ax6e2nd  45485  19.21a3con13vVD  45778  tratrbVD  45787  ssralv2VD  45792  ax6e2ndVD  45834  ax6e2ndALT  45856  stoweidlem35  46967  eu2ndop1stv  48117