Axiom ax-5 1910

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

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

This axiom is referenced by:  ax5d  1911  ax5e  1912  ax5ea  1913  alimdv  1916  eximdv  1917  albidv  1920  exbidv  1921  alrimiv  1927  alrimdv  1929  nexdv  1936  stdpc5v  1938  19.23v  1942  19.37imv  1947  spvw  1980  19.3v  1981  19.8v  1982  spimevw  1994  spimvw  1995  spw  2033  cbvalvw  2035  alcomimw  2042  hbn1w  2046  naev2  2061  sbv  2088  ax12wlem  2132  nf5dv  2148  ax12v  2178  cleljustALT  2367  dvelim  2456  dvelimv  2457  axc16ALT  2494  eujustALT  2572  eqabbOLD  2882  ralrimiv  3145  mpteq12  5234  hashgt23el  14463  bnj1096  34796  bnj1350  34839  bnj1351  34840  bnj1352  34841  bnj1468  34860  bnj1000  34955  bnj1311  35038  bnj1445  35058  bnj1523  35085  umgr2cycllem  35145  umgr2cycl  35146  bj-ax12wlem  36645  bj-cbvalim  36646  bj-cbvexim  36647  bj-cbvexivw  36673  bj-ax12v3  36686  bj-ax12v3ALT  36687  bj-nnfv  36755  bj-abvALT  36908  copsex2b  37141  opelopabbv  37144  brabd  37149  fvineqsnf1  37411  wl-nfalv  37526  mpobi123f  38169  mptbi12f  38173  ax5ALT  38908  dveeq2-o  38934  dveeq1-o  38936  ax12el  38943  ax12a2-o  38951  intimasn  43670  alrim3con13v  44553  ax6e2nd  44578  19.21a3con13vVD  44872  tratrbVD  44881  ssralv2VD  44886  ax6e2ndVD  44928  ax6e2ndALT  44950  stoweidlem35  46050  eu2ndop1stv  47137