HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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
StepHypRef Expression
1 wph . . . 4 wff ph
2 vy . . . 4 set y
31, 2wal 1584 . . 3 wff A.yph
4 vx . . 3 set x
53, 4wal 1584 . 2 wff A.xA.yph
61, 4wal 1584 . . 3 wff A.xph
76, 2wal 1584 . 2 wff A.yA.xph
85, 7wi 3 1 wff (A.xA.yph -> A.yA.xph)
Colors of variables: wff set class
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