Axiom ax-5 1839

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 34192 about the logical redundancy of ax-5 1839 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 2053, 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 1481	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  1840  ax5e  1841  ax5ea  1842  alimdv  1845  eximdv  1846  albidv  1849  exbidv  1850  alrimiv  1855  alrimdv  1857  nexdv  1864  stdpc5v  1867  nfvOLD  1871  19.8v  1895  19.23v  1902  spimvw  1927  spw  1967  cbvalvw  1969  alcomiw  1971  hbn1w  1973  ax12wlem  2009  ax12v  2048  ax12vOLD  2050  ax12vOLDOLD  2051  axc16gOLD  2161  cleljustALT  2185  cbvalv  2273  dvelim  2337  dvelimv  2338  axc16ALT  2366  eujustALT  2473  abeq2  2732  ralrimiv  2965  mpteq12  4736  bnj1096  30853  bnj1350  30896  bnj1351  30897  bnj1352  30898  bnj1468  30916  bnj1000  31011  bnj1311  31092  bnj1445  31112  bnj1523  31139  bj-ax12wlem  32617  bj-spimevw  32657  bj-cbvexivw  32660  bj-ax12v3  32675  bj-ax12v3ALT  32676  bj-sbfvv  32765  bj-abeq2  32773  bj-abv  32901  bj-ab0  32902  wl-hbnaev  33305  wl-nfalv  33312  mpt2bi123f  33971  mptbi12f  33975  ax5ALT  34192  dveeq2-o  34218  dveeq1-o  34220  ax12el  34227  ax12a2-o  34235  intimasn  37949  alrim3con13v  38743  ax6e2nd  38774  19.21a3con13vVD  39087  tratrbVD  39097  ssralv2VD  39102  ax6e2ndVD  39144  ax6e2ndALT  39166  stoweidlem35  40252  eu2ndop1stv  41202