Axiom ax-5 1937

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

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

This axiom is referenced by:  ax5d  1938  ax5e  1939  ax5ea  1940  alimdv  1943  eximdv  1944  albidv  1947  exbidv  1948  alrimiv  1954  alrimdv  1956  nexdv  1963  stdpc5v  1965  19.23v  1969  19.37imv  1974  spvw  2008  19.3v  2009  19.8v  2010  spimevw  2012  spimvw  2013  spw  2061  cbvalvw  2063  alcomimw  2070  hbn1w  2075  naev2  2090  sbv  2128  ax12wlem  2173  nf5dv  2189  ax12v  2220  cleljustALT  2402  dvelim  2489  dvelimv  2490  axc16ALT  2527  eujustALT  2606  ralrimiv  3162  mpteq12  5203  hashgt23el  14461  bnj1096  35116  bnj1350  35158  bnj1351  35159  bnj1352  35160  bnj1468  35179  bnj1000  35274  bnj1311  35357  bnj1445  35377  bnj1523  35404  umgr2cycllem  35565  umgr2cycl  35566  bj-spvw  37180  bj-spvew  37181  bj-alextruim  37182  bj-cbvalvv  37184  bj-ax12wlem  37190  bj-cbvexivw  37218  bj-ax12v3  37233  bj-ax12v3ALT  37234  bj-nnfv  37316  bj-nnfbd  37317  bj-nnf-cbvaliv  37324  bj-abvALT  37465  copsex2b  37706  opelopabbv  37709  brabd  37714  fvineqsnf1  37978  wl-nfalv  38102  mpobi123f  38735  mptbi12f  38739  ecqmap  39022  ax5ALT  39605  dveeq2-o  39631  dveeq1-o  39633  ax12el  39640  ax12a2-o  39648  intimasn  44309  alrim3con13v  45168  ax6e2nd  45193  19.21a3con13vVD  45486  tratrbVD  45495  ssralv2VD  45500  ax6e2ndVD  45542  ax6e2ndALT  45564  stoweidlem35  46675  eu2ndop1stv  47785