Axiom ax-5 1909

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

This axiom is referenced by:  ax5d  1910  ax5e  1911  ax5ea  1912  alimdv  1915  eximdv  1916  albidv  1919  exbidv  1920  alrimiv  1926  alrimdv  1928  nexdv  1935  stdpc5v  1937  19.23v  1941  19.37imv  1947  spvw  1980  19.3v  1981  19.8v  1982  spimevw  1994  spimvw  1995  spw  2033  cbvalvw  2035  alcomimw  2042  hbn1w  2046  naev2  2061  sbv  2088  ax12wlem  2132  nf5dv  2148  ax12v  2179  cleljustALT  2370  dvelim  2459  dvelimv  2460  axc16ALT  2497  eujustALT  2575  eqabbOLD  2885  ralrimiv  3151  mpteq12  5258  hashgt23el  14473  bnj1096  34758  bnj1350  34801  bnj1351  34802  bnj1352  34803  bnj1468  34822  bnj1000  34917  bnj1311  35000  bnj1445  35020  bnj1523  35047  umgr2cycllem  35108  umgr2cycl  35109  bj-ax12wlem  36610  bj-cbvalim  36611  bj-cbvexim  36612  bj-cbvexivw  36638  bj-ax12v3  36651  bj-ax12v3ALT  36652  bj-nnfv  36720  bj-abvALT  36873  copsex2b  37106  opelopabbv  37109  brabd  37114  fvineqsnf1  37376  wl-nfalv  37479  mpobi123f  38122  mptbi12f  38126  ax5ALT  38863  dveeq2-o  38889  dveeq1-o  38891  ax12el  38898  ax12a2-o  38906  intimasn  43619  alrim3con13v  44504  ax6e2nd  44529  19.21a3con13vVD  44823  tratrbVD  44832  ssralv2VD  44837  ax6e2ndVD  44879  ax6e2ndALT  44901  stoweidlem35  45956  eu2ndop1stv  47040