Axiom ax-5 1905

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

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

This axiom is referenced by:  ax5d  1906  ax5e  1907  ax5ea  1908  alimdv  1911  eximdv  1912  albidv  1915  exbidv  1916  alrimiv  1922  alrimdv  1924  nexdv  1931  stdpc5v  1933  19.23v  1937  19.37imv  1943  spvw  1976  19.3v  1977  19.8v  1978  spimevw  1990  spimvw  1991  spw  2029  cbvalvw  2031  alcomiw  2038  hbn1w  2041  naev2  2056  sbv  2083  ax12wlem  2120  nf5dv  2136  ax12v  2167  cleljustALT  2355  dvelim  2444  dvelimv  2445  axc16ALT  2482  eujustALT  2560  eqabbOLD  2866  ralrimiv  3134  mpteq12  5241  hashgt23el  14419  bnj1096  34544  bnj1350  34587  bnj1351  34588  bnj1352  34589  bnj1468  34608  bnj1000  34703  bnj1311  34786  bnj1445  34806  bnj1523  34833  umgr2cycllem  34881  umgr2cycl  34882  bj-ax12wlem  36251  bj-cbvalim  36252  bj-cbvexim  36253  bj-cbvexivw  36279  bj-ax12v3  36293  bj-ax12v3ALT  36294  bj-nnfv  36362  bj-abvALT  36516  copsex2b  36750  opelopabbv  36753  brabd  36758  fvineqsnf1  37020  wl-nfalv  37123  mpobi123f  37766  mptbi12f  37770  ax5ALT  38509  dveeq2-o  38535  dveeq1-o  38537  ax12el  38544  ax12a2-o  38552  intimasn  43229  alrim3con13v  44114  ax6e2nd  44139  19.21a3con13vVD  44433  tratrbVD  44442  ssralv2VD  44447  ax6e2ndVD  44489  ax6e2ndALT  44511  stoweidlem35  45561  eu2ndop1stv  46643