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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2221. (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  2216  cleljustALT  2395  dvelim  2482  dvelimv  2483  axc16ALT  2520  eujustALT  2599  ralrimiv  3155  mpteq12  5197  hashgt23el  14489  umgr2cycllem  30609  umgr2cycl  30610  bnj1096  35277  bnj1350  35319  bnj1351  35320  bnj1352  35321  bnj1468  35340  bnj1000  35435  bnj1311  35518  bnj1445  35538  bnj1523  35565  bj-spvw  37350  bj-spvew  37351  bj-alextruim  37352  bj-cbvalvv  37354  bj-ax12wlem  37360  bj-cbvexivw  37388  bj-ax12v3  37403  bj-ax12v3ALT  37404  bj-nnfv  37486  bj-nnfbd  37487  bj-nnf-cbvaliv  37494  bj-abvALT  37635  copsex2b  37877  opelopabbv  37880  brabd  37885  fvineqsnf1  38149  wl-nfalv  38273  findcard4  38448  mpobi123f  38895  mptbi12f  38899  ecqmap  39182  ax5ALT  39765  dveeq2-o  39791  dveeq1-o  39793  ax12el  39800  ax12a2-o  39808  intimasn  44482  alrim3con13v  45341  ax6e2nd  45366  19.21a3con13vVD  45659  tratrbVD  45668  ssralv2VD  45673  ax6e2ndVD  45715  ax6e2ndALT  45737  stoweidlem35  46848  eu2ndop1stv  47998