Axiom ax-5 1911

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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2182. (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  1912  ax5e  1913  ax5ea  1914  alimdv  1917  eximdv  1918  albidv  1921  exbidv  1922  alrimiv  1928  alrimdv  1930  nexdv  1937  stdpc5v  1939  19.23v  1943  19.37imv  1948  spvw  1985  19.3v  1986  19.8v  1987  spimevw  2001  spimvw  2002  spw  2041  cbvalvw  2043  alcomiw  2050  alcomiwOLD  2051  hbn1w  2053  naev2  2066  sbv  2098  ax12wlem  2136  nf5dv  2152  ax12v  2178  cleljustALT  2382  cbvalvOLD  2420  dvelim  2473  dvelimv  2474  axc16ALT  2528  eujustALT  2657  abeq2  2945  ralrimiv  3181  mpteq12  5153  hashgt23el  13786  bnj1096  32054  bnj1350  32097  bnj1351  32098  bnj1352  32099  bnj1468  32118  bnj1000  32213  bnj1311  32296  bnj1445  32316  bnj1523  32343  umgr2cycllem  32387  umgr2cycl  32388  bj-ax12wlem  33977  bj-cbvalim  33978  bj-cbvexim  33979  bj-cbvexivw  34005  bj-ax12v3  34019  bj-ax12v3ALT  34020  bj-nnfv  34083  bj-abv  34226  bj-ab0  34227  copsex2b  34435  opelopabbv  34438  brabd  34443  fvineqsnf1  34694  wl-nfalv  34780  mpobi123f  35455  mptbi12f  35459  ax5ALT  36058  dveeq2-o  36084  dveeq1-o  36086  ax12el  36093  ax12a2-o  36101  intimasn  40022  alrim3con13v  40887  ax6e2nd  40912  19.21a3con13vVD  41206  tratrbVD  41215  ssralv2VD  41220  ax6e2ndVD  41262  ax6e2ndALT  41284  stoweidlem35  42340  eu2ndop1stv  43344