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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2183. (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  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  2178  cleljustALT  2366  dvelim  2455  dvelimv  2456  axc16ALT  2493  eujustALT  2571  eqabbOLD  2875  ralrimiv  3131  mpteq12  5208  hashgt23el  14440  bnj1096  34759  bnj1350  34802  bnj1351  34803  bnj1352  34804  bnj1468  34823  bnj1000  34918  bnj1311  35001  bnj1445  35021  bnj1523  35048  umgr2cycllem  35108  umgr2cycl  35109  bj-ax12wlem  36608  bj-cbvalim  36609  bj-cbvexim  36610  bj-cbvexivw  36636  bj-ax12v3  36649  bj-ax12v3ALT  36650  bj-nnfv  36718  bj-abvALT  36871  copsex2b  37104  opelopabbv  37107  brabd  37112  fvineqsnf1  37374  wl-nfalv  37489  mpobi123f  38132  mptbi12f  38136  ax5ALT  38871  dveeq2-o  38897  dveeq1-o  38899  ax12el  38906  ax12a2-o  38914  intimasn  43628  alrim3con13v  44506  ax6e2nd  44531  19.21a3con13vVD  44824  tratrbVD  44833  ssralv2VD  44838  ax6e2ndVD  44880  ax6e2ndALT  44902  stoweidlem35  46012  eu2ndop1stv  47102