Theorem ax11-pm2 33159

Description: Proof of ax-11 2190 from the standard axioms of predicate calculus, similar to PM's proof of alcom 2193 (PM*11.2). This proof requires that 𝑥 and 𝑦 be distinct. Axiom ax-11 2190 is used in the proof only through nfal 2317, nfsb 2590, sbal 2610, sb8 2571. See also ax11-pm 33155. (Contributed by BJ, 15-Sep-2018.) (Proof modification is discouraged.)

Assertion

Ref	Expression
ax11-pm2	⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem ax11-pm2

Dummy variables 𝑧 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2stdpc4 2500	. . . . . 6 ⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑)
2	1	gen2 1871	. . . . 5 ⊢ ∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑)
3		nfv 1995	. . . . . . . 8 ⊢ Ⅎ𝑡𝜑
4	3	nfal 2317	. . . . . . 7 ⊢ Ⅎ𝑡∀𝑦𝜑
5	4	nfal 2317	. . . . . 6 ⊢ Ⅎ𝑡∀𝑥∀𝑦𝜑
6		nfv 1995	. . . . . . . 8 ⊢ Ⅎ𝑧𝜑
7	6	nfal 2317	. . . . . . 7 ⊢ Ⅎ𝑧∀𝑦𝜑
8	7	nfal 2317	. . . . . 6 ⊢ Ⅎ𝑧∀𝑥∀𝑦𝜑
9	5, 8	2stdpc5 33152	. . . . 5 ⊢ (∀𝑡∀𝑧(∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑡 / 𝑦]𝜑) → (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑))
10	2, 9	ax-mp 5	. . . 4 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)
11	6	nfsb 2590	. . . . . 6 ⊢ Ⅎ𝑧[𝑡 / 𝑦]𝜑
12	11	sb8 2571	. . . . 5 ⊢ (∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)
13	12	albii 1895	. . . 4 ⊢ (∀𝑡∀𝑥[𝑡 / 𝑦]𝜑 ↔ ∀𝑡∀𝑧[𝑧 / 𝑥][𝑡 / 𝑦]𝜑)
14	10, 13	sylibr 224	. . 3 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑)
15		sbal 2610	. . . 4 ⊢ ([𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑡 / 𝑦]𝜑)
16	15	albii 1895	. . 3 ⊢ (∀𝑡[𝑡 / 𝑦]∀𝑥𝜑 ↔ ∀𝑡∀𝑥[𝑡 / 𝑦]𝜑)
17	14, 16	sylibr 224	. 2 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑)
18	3	nfal 2317	. . 3 ⊢ Ⅎ𝑡∀𝑥𝜑
19	18	sb8 2571	. 2 ⊢ (∀𝑦∀𝑥𝜑 ↔ ∀𝑡[𝑡 / 𝑦]∀𝑥𝜑)
20	17, 19	sylibr 224	1 ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1629  [wsb 2049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050

This theorem is referenced by: (None)