Axiom ax-7d

Description: Distinct variable version of ax-11 . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	ax-7d	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )

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	⊢ ( ∀ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )