Theorem pm11.58

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

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

Proof

Step	Hyp	Ref	Expression
1		19.8a	⊢ ( 𝜑 → ∃ 𝑥 𝜑 )
2		nfv	⊢ Ⅎ 𝑦 𝜑
3	2	sb8e	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
4	1 3	sylib	⊢ ( 𝜑 → ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
5	4	pm4.71i	⊢ ( 𝜑 ↔ ( 𝜑 ∧ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
6		19.42v	⊢ ( ∃ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜑 ∧ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
7	5 6	bitr4i	⊢ ( 𝜑 ↔ ∃ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
8	7	exbii	⊢ ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )