Axiom ax-5 1932

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 39536 about the logical redundancy of ax-5 1932 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 2220, we can also remove the quantifier (unconditionally).

For an explanation of disjoint variable conditions, see https://us.metamath.org/mpeuni/mmset.html#distinct 2220. (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 1560	. 2 wff ∀𝑥𝜑
4	1, 3	wi 4	1 wff (𝜑 → ∀𝑥𝜑)

This axiom is referenced by:  ax5d  1933  ax5e  1934  ax5ea  1935  alimdv  1938  eximdv  1939  albidv  1942  exbidv  1943  alrimiv  1949  alrimdv  1951  nexdv  1958  stdpc5v  1960  19.23v  1964  19.37imv  1969  spvw  2003  19.3v  2004  19.8v  2005  spimevw  2007  spimvw  2008  spw  2056  cbvalvw  2058  alcomimw  2065  hbn1w  2070  naev2  2085  sbv  2123  ax12wlem  2168  nf5dv  2184  ax12v  2215  cleljustALT  2397  dvelim  2484  dvelimv  2485  axc16ALT  2522  eujustALT  2601  ralrimiv  3155  mpteq12  5190  hashgt23el  14439  bnj1096  35080  bnj1350  35122  bnj1351  35123  bnj1352  35124  bnj1468  35143  bnj1000  35238  bnj1311  35321  bnj1445  35341  bnj1523  35368  umgr2cycllem  35495  umgr2cycl  35496  bj-spvw  37112  bj-spvew  37113  bj-alextruim  37114  bj-cbvalvv  37116  bj-ax12wlem  37122  bj-cbvexivw  37150  bj-ax12v3  37165  bj-ax12v3ALT  37166  bj-nnfv  37248  bj-nnfbd  37249  bj-nnf-cbvaliv  37256  bj-abvALT  37397  copsex2b  37637  opelopabbv  37640  brabd  37645  fvineqsnf1  37909  wl-nfalv  38033  mpobi123f  38666  mptbi12f  38670  ecqmap  38953  ax5ALT  39536  dveeq2-o  39562  dveeq1-o  39564  ax12el  39571  ax12a2-o  39579  intimasn  44238  alrim3con13v  45114  ax6e2nd  45139  19.21a3con13vVD  45432  tratrbVD  45441  ssralv2VD  45446  ax6e2ndVD  45488  ax6e2ndALT  45510  stoweidlem35  46614  eu2ndop1stv  47724