Axiom ax-5 1938

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

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

This axiom is referenced by:  ax5d  1939  ax5e  1940  ax5ea  1941  alimdv  1944  eximdv  1945  albidv  1948  exbidv  1949  alrimiv  1955  alrimdv  1957  nexdv  1964  stdpc5v  1966  19.23v  1970  19.37imv  1975  spvw  2009  19.3v  2010  19.8v  2011  spimevw  2013  spimvw  2014  spw  2062  cbvalvw  2064  alcomimw  2071  hbn1w  2076  naev2  2091  sbv  2120  ax12wlem  2165  nf5dv  2181  ax12v  2212  cleljustALT  2394  dvelim  2481  dvelimv  2482  axc16ALT  2519  eujustALT  2598  ralrimiv  3154  mpteq12  5198  hashgt23el  14460  bnj1096  35137  bnj1350  35179  bnj1351  35180  bnj1352  35181  bnj1468  35200  bnj1000  35295  bnj1311  35378  bnj1445  35398  bnj1523  35425  umgr2cycllem  35586  umgr2cycl  35587  bj-spvw  37201  bj-spvew  37202  bj-alextruim  37203  bj-cbvalvv  37205  bj-ax12wlem  37211  bj-cbvexivw  37239  bj-ax12v3  37254  bj-ax12v3ALT  37255  bj-nnfv  37337  bj-nnfbd  37338  bj-nnf-cbvaliv  37345  bj-abvALT  37486  copsex2b  37728  opelopabbv  37731  brabd  37736  fvineqsnf1  38000  wl-nfalv  38124  mpobi123f  38757  mptbi12f  38761  ecqmap  39044  ax5ALT  39627  dveeq2-o  39653  dveeq1-o  39655  ax12el  39662  ax12a2-o  39670  intimasn  44331  alrim3con13v  45190  ax6e2nd  45215  19.21a3con13vVD  45508  tratrbVD  45517  ssralv2VD  45522  ax6e2ndVD  45564  ax6e2ndALT  45586  stoweidlem35  46697  eu2ndop1stv  47807