Axiom ax-7 1592

Description: Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. One of the 4 axioms of pure predicate calculus. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of [Monk2] p. 113. An alternate axiomatization could use ax467 1659 in place of ax-4 1608, ax-6o 1613, and ax-7 1592.

Assertion

Ref	Expression
ax-7	|- (A.xA.yph -> A.yA.xph)

Detailed syntax breakdown of Axiom ax-7

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff ph
2		vy	. . . 4 set y
3	1, 2	wal 1584	. . 3 wff A.yph
4		vx	. . 3 set x
5	3, 4	wal 1584	. 2 wff A.xA.yph
6	1, 4	wal 1584	. . 3 wff A.xph
7	6, 2	wal 1584	. 2 wff A.yA.xph
8	5, 7	wi 3	1 wff (A.xA.yph -> A.yA.xph)

This axiom is referenced by:  a7s 1626  hbal 1641  ax67 1656  ax467 1659  alcom 1668  hbald 1753  hbae 1786  cbv1 1804  sbal1 2001  ax11indalem 2023  ax11inda2ALT 2024  hbabd 2133  hbaltg 14515  pm11.71 17178  ax4567 17183  ax10ext 17188

Copyright terms: Public domain