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 36929 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  3107  mpteq12  5165  hashgt23el  14149  bnj1096  32770  bnj1350  32813  bnj1351  32814  bnj1352  32815  bnj1468  32834  bnj1000  32929  bnj1311  33012  bnj1445  33032  bnj1523  33059  umgr2cycllem  33110  umgr2cycl  33111  bj-ax12wlem  34833  bj-cbvalim  34834  bj-cbvexim  34835  bj-cbvexivw  34861  bj-ax12v3  34875  bj-ax12v3ALT  34876  bj-nnfv  34944  bj-abvALT  35100  copsex2b  35319  opelopabbv  35322  brabd  35327  fvineqsnf1  35589  wl-nfalv  35692  mpobi123f  36328  mptbi12f  36332  ax5ALT  36929  dveeq2-o  36955  dveeq1-o  36957  ax12el  36964  ax12a2-o  36972  intimasn  41246  alrim3con13v  42134  ax6e2nd  42159  19.21a3con13vVD  42453  tratrbVD  42462  ssralv2VD  42467  ax6e2ndVD  42509  ax6e2ndALT  42531  stoweidlem35  43557  eu2ndop1stv  44595