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 38890 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  5180  hashgt23el  14331  bnj1096  34749  bnj1350  34792  bnj1351  34793  bnj1352  34794  bnj1468  34813  bnj1000  34908  bnj1311  34991  bnj1445  35011  bnj1523  35038  umgr2cycllem  35117  umgr2cycl  35118  bj-ax12wlem  36622  bj-cbvalim  36623  bj-cbvexim  36624  bj-cbvexivw  36650  bj-ax12v3  36663  bj-ax12v3ALT  36664  bj-nnfv  36732  bj-abvALT  36885  copsex2b  37118  opelopabbv  37121  brabd  37126  fvineqsnf1  37388  wl-nfalv  37503  mpobi123f  38146  mptbi12f  38150  ax5ALT  38890  dveeq2-o  38916  dveeq1-o  38918  ax12el  38925  ax12a2-o  38933  intimasn  43634  alrim3con13v  44511  ax6e2nd  44536  19.21a3con13vVD  44829  tratrbVD  44838  ssralv2VD  44843  ax6e2ndVD  44885  ax6e2ndALT  44907  stoweidlem35  46020  eu2ndop1stv  47113