Axiom ax-5 1827

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 33210 about the logical redundancy of ax-5 1827 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 2041, 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 1473	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  1828  ax5e  1829  nfv  1830  alimdv  1832  eximdv  1833  albidv  1836  exbidv  1837  alrimiv  1842  alrimdv  1844  nexdv  1851  stdpc5v  1854  nfvOLD  1858  19.8v  1882  19.23v  1889  spimvw  1914  spw  1954  cbvalvw  1956  alcomiw  1958  hbn1w  1960  ax12wlem  1996  ax12v  2035  ax12vOLD  2037  ax12vOLDOLD  2038  axc16gOLD  2147  cleljustALT  2173  dvelim  2325  dvelimv  2326  axc16ALT  2354  eujustALT  2461  abeq2  2719  ralrimiv  2948  mpteq12  4664  bnj1096  30107  bnj1350  30150  bnj1351  30151  bnj1352  30152  bnj1468  30170  bnj1000  30265  bnj1311  30346  bnj1445  30366  bnj1523  30393  bj-ax5ea  31805  bj-ax12wlem  31807  bj-spimevw  31844  bj-cbvexivw  31847  bj-ax12v3  31862  bj-ax12v3ALT  31863  bj-sbfvv  31953  bj-abeq2  31961  bj-abv  32093  bj-ab0  32094  wl-hbnaev  32484  wl-nfalv  32491  mpt2bi123f  33141  mptbi12f  33145  ax5ALT  33210  dveeq2-o  33236  dveeq1-o  33238  ax12el  33245  ax12a2-o  33253  intimasn  36968  alrim3con13v  37764  ax6e2nd  37795  19.21a3con13vVD  38109  tratrbVD  38119  ssralv2VD  38124  ax6e2ndVD  38166  ax6e2ndALT  38188  stoweidlem35  38928  eu2ndop1stv  39851