Theorem pm11.57

Description: Theorem *11.57 in WhiteheadRussell p. 165. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	pm11.57	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑦 𝜑
2	1	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 𝜑
3		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
4		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
5	3 4	jca	⊢ ( ∀ 𝑥 𝜑 → ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
6	2 5	alrimi	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
7	6	axc4i	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
8		simpl	⊢ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝜑 )
9	8	sps	⊢ ( ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝜑 )
10	9	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ∀ 𝑥 𝜑 )
11	7 10	impbii	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )