Axiom ax-5 1910

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

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

This axiom is referenced by:  ax5d  1911  ax5e  1912  ax5ea  1913  alimdv  1916  eximdv  1917  albidv  1920  exbidv  1921  alrimiv  1927  alrimdv  1929  nexdv  1936  stdpc5v  1938  19.23v  1942  19.37imv  1947  spvw  1981  19.3v  1982  19.8v  1983  spimevw  1985  spimvw  1986  spw  2034  cbvalvw  2036  alcomimw  2043  hbn1w  2047  naev2  2062  sbv  2089  ax12wlem  2133  nf5dv  2149  ax12v  2179  cleljustALT  2362  dvelim  2449  dvelimv  2450  axc16ALT  2487  eujustALT  2565  eqabbOLD  2868  ralrimiv  3120  mpteq12  5183  hashgt23el  14349  bnj1096  34751  bnj1350  34794  bnj1351  34795  bnj1352  34796  bnj1468  34815  bnj1000  34910  bnj1311  34993  bnj1445  35013  bnj1523  35040  umgr2cycllem  35115  umgr2cycl  35116  bj-ax12wlem  36620  bj-cbvalim  36621  bj-cbvexim  36622  bj-cbvexivw  36648  bj-ax12v3  36661  bj-ax12v3ALT  36662  bj-nnfv  36730  bj-abvALT  36883  copsex2b  37116  opelopabbv  37119  brabd  37124  fvineqsnf1  37386  wl-nfalv  37501  mpobi123f  38144  mptbi12f  38148  ax5ALT  38888  dveeq2-o  38914  dveeq1-o  38916  ax12el  38923  ax12a2-o  38931  intimasn  43633  alrim3con13v  44510  ax6e2nd  44535  19.21a3con13vVD  44828  tratrbVD  44837  ssralv2VD  44842  ax6e2ndVD  44884  ax6e2ndALT  44906  stoweidlem35  46020  eu2ndop1stv  47113