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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2180. (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 1536	. 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  2095  ax12wlem  2133  nf5dv  2149  ax12v  2176  cleljustALT  2371  cbvalvOLD  2409  dvelim  2462  dvelimv  2463  axc16ALT  2507  eujustALT  2632  abeq2  2922  ralrimiv  3148  mpteq12  5117  hashgt23el  13781  bnj1096  32164  bnj1350  32207  bnj1351  32208  bnj1352  32209  bnj1468  32228  bnj1000  32323  bnj1311  32406  bnj1445  32426  bnj1523  32453  umgr2cycllem  32500  umgr2cycl  32501  bj-ax12wlem  34090  bj-cbvalim  34091  bj-cbvexim  34092  bj-cbvexivw  34118  bj-ax12v3  34132  bj-ax12v3ALT  34133  bj-nnfv  34198  bj-abv  34347  bj-ab0  34348  copsex2b  34555  opelopabbv  34558  brabd  34563  fvineqsnf1  34827  wl-nfalv  34930  mpobi123f  35600  mptbi12f  35604  ax5ALT  36203  dveeq2-o  36229  dveeq1-o  36231  ax12el  36238  ax12a2-o  36246  intimasn  40358  alrim3con13v  41239  ax6e2nd  41264  19.21a3con13vVD  41558  tratrbVD  41567  ssralv2VD  41572  ax6e2ndVD  41614  ax6e2ndALT  41636  stoweidlem35  42677  eu2ndop1stv  43681