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

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2186. (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 1539	. 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  1982  19.3v  1983  19.8v  1984  spimevw  1986  spimvw  1987  spw  2035  cbvalvw  2037  alcomimw  2044  hbn1w  2049  naev2  2064  sbv  2091  ax12wlem  2135  nf5dv  2151  ax12v  2181  cleljustALT  2364  dvelim  2451  dvelimv  2452  axc16ALT  2489  eujustALT  2567  eqabbOLD  2871  ralrimiv  3123  mpteq12  5177  hashgt23el  14331  bnj1096  34794  bnj1350  34837  bnj1351  34838  bnj1352  34839  bnj1468  34858  bnj1000  34953  bnj1311  35036  bnj1445  35056  bnj1523  35083  umgr2cycllem  35184  umgr2cycl  35185  bj-ax12wlem  36688  bj-cbvalim  36689  bj-cbvexim  36690  bj-cbvexivw  36716  bj-ax12v3  36729  bj-ax12v3ALT  36730  bj-nnfv  36798  bj-abvALT  36951  copsex2b  37184  opelopabbv  37187  brabd  37192  fvineqsnf1  37454  wl-nfalv  37569  mpobi123f  38212  mptbi12f  38216  ax5ALT  39016  dveeq2-o  39042  dveeq1-o  39044  ax12el  39051  ax12a2-o  39059  intimasn  43760  alrim3con13v  44636  ax6e2nd  44661  19.21a3con13vVD  44954  tratrbVD  44963  ssralv2VD  44968  ax6e2ndVD  45010  ax6e2ndALT  45032  stoweidlem35  46143  eu2ndop1stv  47235