Axiom ax-5 1991

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 34713 about the logical redundancy of ax-5 1991 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 2207, 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 1629	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  1992  ax5e  1993  ax5ea  1994  alimdv  1997  eximdv  1998  albidv  2001  exbidv  2002  alrimiv  2007  alrimdv  2009  nexdv  2016  stdpc5v  2019  19.23v  2023  19.37imv  2027  nfvOLD  2040  19.8v  2064  19.23vOLD  2071  spimvw  2085  spw  2123  cbvalvw  2125  alcomiw  2127  alcomiwOLD  2128  hbn1w  2130  ax12wlem  2164  nf5dv  2181  ax12v  2204  axc16gOLD  2324  cleljustALT  2347  cbvalv  2434  dvelim  2487  dvelimv  2488  axc16ALT  2513  eujustALT  2621  abeq2  2881  ralrimiv  3114  mpteq12  4871  bnj1096  31191  bnj1350  31234  bnj1351  31235  bnj1352  31236  bnj1468  31254  bnj1000  31349  bnj1311  31430  bnj1445  31450  bnj1523  31477  bj-ax12wlem  32954  bj-spimevw  32993  bj-cbvexivw  32996  bj-ax12v3  33011  bj-ax12v3ALT  33012  bj-sbfvv  33100  bj-abeq2  33108  bj-abv  33229  bj-ab0  33230  wl-hbnaev  33641  wl-nfalv  33646  mpt2bi123f  34301  mptbi12f  34305  ax5ALT  34713  dveeq2-o  34739  dveeq1-o  34741  ax12el  34748  ax12a2-o  34756  intimasn  38473  alrim3con13v  39266  ax6e2nd  39297  19.21a3con13vVD  39607  tratrbVD  39617  ssralv2VD  39622  ax6e2ndVD  39664  ax6e2ndALT  39686  stoweidlem35  40764  eu2ndop1stv  41717