ax-5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ax-5		Structured version Visualization version GIF version

Axiom ax-5 1906

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

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

Colors of variables: wff setvar class

This axiom is referenced by: ax5d 1907 ax5e 1908 ax5ea 1909 alimdv 1912 eximdv 1913 albidv 1916 exbidv 1917 alrimiv 1923 alrimdv 1925 nexdv 1932 stdpc5v 1934 19.23v 1938 19.37imv 1944 spvw 1977 19.3v 1978 19.8v 1979 spimevw 1991 spimvw 1992 spw 2030 cbvalvw 2032 alcomiw 2039 hbn1w 2042 naev2 2057 sbv 2084 ax12wlem 2121 nf5dv 2137 ax12v 2168 cleljustALT 2356 dvelim 2445 dvelimv 2446 axc16ALT 2483 eujustALT 2561 eqabbOLD 2867 ralrimiv 3135 mpteq12 5245 hashgt23el 14441 bnj1096 34627 bnj1350 34670 bnj1351 34671 bnj1352 34672 bnj1468 34691 bnj1000 34786 bnj1311 34869 bnj1445 34889 bnj1523 34916 umgr2cycllem 34968 umgr2cycl 34969 bj-ax12wlem 36348 bj-cbvalim 36349 bj-cbvexim 36350 bj-cbvexivw 36376 bj-ax12v3 36390 bj-ax12v3ALT 36391 bj-nnfv 36459 bj-abvALT 36613 copsex2b 36847 opelopabbv 36850 brabd 36855 fvineqsnf1 37117 wl-nfalv 37220 mpobi123f 37863 mptbi12f 37867 ax5ALT 38605 dveeq2-o 38631 dveeq1-o 38633 ax12el 38640 ax12a2-o 38648 intimasn 43324 alrim3con13v 44209 ax6e2nd 44234 19.21a3con13vVD 44528 tratrbVD 44537 ssralv2VD 44542 ax6e2ndVD 44584 ax6e2ndALT 44606 stoweidlem35 45656 eu2ndop1stv 46738

W3C validator

	
		OSZAR »