Axiom ax-5 1907

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

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

This axiom is referenced by:  ax5d  1908  ax5e  1909  ax5ea  1910  alimdv  1913  eximdv  1914  albidv  1917  exbidv  1918  alrimiv  1924  alrimdv  1926  nexdv  1933  stdpc5v  1935  19.23v  1939  19.37imv  1944  spvw  1977  19.3v  1978  19.8v  1979  spimevw  1991  spimvw  1992  spw  2030  cbvalvw  2032  alcomimw  2039  hbn1w  2043  naev2  2058  sbv  2085  ax12wlem  2129  nf5dv  2145  ax12v  2175  cleljustALT  2364  dvelim  2453  dvelimv  2454  axc16ALT  2491  eujustALT  2569  eqabbOLD  2879  ralrimiv  3142  mpteq12  5239  hashgt23el  14459  bnj1096  34774  bnj1350  34817  bnj1351  34818  bnj1352  34819  bnj1468  34838  bnj1000  34933  bnj1311  35016  bnj1445  35036  bnj1523  35063  umgr2cycllem  35124  umgr2cycl  35125  bj-ax12wlem  36626  bj-cbvalim  36627  bj-cbvexim  36628  bj-cbvexivw  36654  bj-ax12v3  36667  bj-ax12v3ALT  36668  bj-nnfv  36736  bj-abvALT  36889  copsex2b  37122  opelopabbv  37125  brabd  37130  fvineqsnf1  37392  wl-nfalv  37505  mpobi123f  38148  mptbi12f  38152  ax5ALT  38888  dveeq2-o  38914  dveeq1-o  38916  ax12el  38923  ax12a2-o  38931  intimasn  43646  alrim3con13v  44530  ax6e2nd  44555  19.21a3con13vVD  44849  tratrbVD  44858  ssralv2VD  44863  ax6e2ndVD  44905  ax6e2ndALT  44927  stoweidlem35  45990  eu2ndop1stv  47074