Axiom ax-5 1942

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 40007 about the logical redundancy of ax-5 1942 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 1567	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is used by:  ax5d  1943  ax5e  1944  ax5ea  1945  alimdv  1948  eximdv  1949  albidv  1952  exbidv  1953  alrimiv  1959  alrimdv  1961  nexdv  1968  stdpc5v  1970  19.23v  1974  19.37imv  1979  spvw  2013  19.3v  2014  19.8v  2015  spimevw  2017  spimvw  2018  spw  2066  cbvalvw  2068  alcomimw  2075  hbn1w  2080  naev2  2095  sbv  2124  ax12wlem  2168  nf5dv  2184  ax12v  2213  cleljustALT  2393  dvelim  2480  dvelimv  2481  axc16ALT  2518  eujustALT  2597  ralrimiv  3153  mpteq12  5192  hashgt23el  14569  umgr2cycllem  30746  umgr2cycl  30747  bnj1096  35455  bnj1350  35497  bnj1351  35498  bnj1352  35499  bnj1468  35518  bnj1000  35613  bnj1311  35696  bnj1445  35716  bnj1523  35743  bj-spvw  37576  bj-spvew  37577  bj-alextruim  37578  bj-cbvalvv  37580  bj-ax12wlem  37586  bj-cbvexivw  37614  bj-ax12v3  37629  bj-ax12v3ALT  37630  bj-nnfv  37712  bj-nnfbd  37713  bj-nnf-cbvaliv  37720  bj-abvALT  37861  copsex2b  38104  opelopabbv  38107  brabd  38112  fvineqsnf1  38376  wl-nfalv  38500  findcard4  38675  mpobi123f  39137  mptbi12f  39141  ecqmap  39424  ax5ALT  40007  dveeq2-o  40033  dveeq1-o  40035  ax12el  40042  ax12a2-o  40050  intimasn  44699  alrim3con13v  45558  ax6e2nd  45583  19.21a3con13vVD  45876  tratrbVD  45885  ssralv2VD  45890  ax6e2ndVD  45932  ax6e2ndALT  45954  stoweidlem35  47087  eu2ndop1stv  48237