Axiom ax-11 2147

Description: Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. 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. This axiom scheme is logically redundant (see ax11w 2119) but is used as an auxiliary axiom scheme to achieve metalogical completeness. Use its weak version alcomiw 2039 when it allows to avoid dependence on ax-11 2147. (Contributed by NM, 12-Mar-1993.)

Assertion

Ref	Expression
ax-11	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Detailed syntax breakdown of Axiom ax-11

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vy	. . . 4 setvar 𝑦
3	1, 2	wal 1532	. . 3 wff ∀𝑦𝜑
4		vx	. . 3 setvar 𝑥
5	3, 4	wal 1532	. 2 wff ∀𝑥∀𝑦𝜑
6	1, 4	wal 1532	. . 3 wff ∀𝑥𝜑
7	6, 2	wal 1532	. 2 wff ∀𝑦∀𝑥𝜑
8	5, 7	wi 4	1 wff (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

This axiom is referenced by:  alcoms  2148  alcom  2149  hbal  2157  hbald  2158  hbsbwOLD  2162  nfald  2317  hbae  2425  hbaltg  35631  bj-hbalt  36386  bj-nnflemaa  36467  bj-nfald  36844  hbae-o  38601  axc711  38612  axc5c711  38616  ax12indalem  38643  ax12inda2ALT  38644  pm11.71  44071  axc5c4c711  44075  axc11next  44080  hbalg  44231  hbalgVD  44581  hbexgVD  44582  ichal  47038

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »