Axiom ax-5 2009

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 34977 about the logical redundancy of ax-5 2009 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 2224, we can also remove the quantifier (unconditionally). (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 1654	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  2010  ax5e  2011  ax5ea  2012  alimdv  2015  eximdv  2016  albidv  2019  exbidv  2020  alrimiv  2026  alrimdv  2028  nexdv  2035  stdpc5v  2037  19.23v  2041  19.37imv  2046  19.8v  2083  19.23vOLD  2090  spimvw  2103  spw  2141  cbvalvw  2143  alcomiw  2145  alcomiwOLD  2146  hbn1w  2148  hbnaevg  2160  ax12wlem  2183  nf5dv  2199  ax12v  2221  sbequivv  2344  cleljustALT  2384  cbvalv  2425  dvelim  2472  dvelimv  2473  axc16ALT  2497  eujustALT  2643  abeq2  2937  ralrimiv  3174  mpteq12  4961  bnj1096  31395  bnj1350  31438  bnj1351  31439  bnj1352  31440  bnj1468  31458  bnj1000  31553  bnj1311  31634  bnj1445  31654  bnj1523  31681  bj-ax12wlem  33144  bj-cbvalim  33145  bj-cbvexim  33146  bj-spimevw  33191  bj-cbvexivw  33194  bj-ax12v3  33209  bj-ax12v3ALT  33210  bj-sbfvv  33289  bj-abeq2  33295  bj-abv  33417  bj-ab0  33418  wl-nfalv  33851  mpt2bi123f  34506  mptbi12f  34510  ax5ALT  34977  dveeq2-o  35003  dveeq1-o  35005  ax12el  35012  ax12a2-o  35020  intimasn  38785  alrim3con13v  39572  ax6e2nd  39597  19.21a3con13vVD  39901  tratrbVD  39910  ssralv2VD  39915  ax6e2ndVD  39957  ax6e2ndALT  39979  stoweidlem35  41040  eu2ndop1stv  42021