Axiom ax-wl-11v

Description: Version of ax-11 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 . It will later be converted into a theorem directly based on ax-11 . (Contributed by Wolf Lammen, 28-Jun-2019)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		vy	⊢ 𝑦
2		wph	⊢ 𝜑
3	2 1	wal	⊢ ∀ 𝑦 𝜑
4	3 0	wal	⊢ ∀ 𝑥 ∀ 𝑦 𝜑
5	2 0	wal	⊢ ∀ 𝑥 𝜑
6	5 1	wal	⊢ ∀ 𝑦 ∀ 𝑥 𝜑
7	4 6	wi	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )