Axiom ax-5 1913

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

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

This axiom is referenced by:  ax5d  1914  ax5e  1915  ax5ea  1916  alimdv  1919  eximdv  1920  albidv  1923  exbidv  1924  alrimiv  1930  alrimdv  1932  nexdv  1939  stdpc5v  1941  19.23v  1945  19.37imv  1951  spvw  1984  19.3v  1985  19.8v  1986  spimevw  1998  spimvw  1999  spw  2037  cbvalvw  2039  alcomiw  2046  alcomiwOLD  2047  hbn1w  2049  naev2  2064  sbv  2091  ax12wlem  2128  nf5dv  2144  ax12v  2172  cleljustALT  2362  dvelim  2451  dvelimv  2452  axc16ALT  2493  eujustALT  2572  abeq2  2872  ralrimiv  3102  mpteq12  5166  hashgt23el  14139  bnj1096  32762  bnj1350  32805  bnj1351  32806  bnj1352  32807  bnj1468  32826  bnj1000  32921  bnj1311  33004  bnj1445  33024  bnj1523  33051  umgr2cycllem  33102  umgr2cycl  33103  bj-ax12wlem  34825  bj-cbvalim  34826  bj-cbvexim  34827  bj-cbvexivw  34853  bj-ax12v3  34867  bj-ax12v3ALT  34868  bj-nnfv  34936  bj-abvALT  35092  copsex2b  35311  opelopabbv  35314  brabd  35319  fvineqsnf1  35581  wl-nfalv  35684  mpobi123f  36320  mptbi12f  36324  ax5ALT  36921  dveeq2-o  36947  dveeq1-o  36949  ax12el  36956  ax12a2-o  36964  intimasn  41265  alrim3con13v  42153  ax6e2nd  42178  19.21a3con13vVD  42472  tratrbVD  42481  ssralv2VD  42486  ax6e2ndVD  42528  ax6e2ndALT  42550  stoweidlem35  43576  eu2ndop1stv  44617