Theorem pm14.24

Description: Theorem *14.24 in WhiteheadRussell p. 191. (Contributed by Andrew Salmon, 12-Jul-2011)

	Ref	Expression
Assertion	pm14.24	⊢ ( ∃! 𝑥 𝜑 → ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = ( ℩ 𝑥 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfeu1	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑
2		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
3		pm14.12	⊢ ( ∃! 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
4	3	19.21bbi	⊢ ( ∃! 𝑥 𝜑 → ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
5	4	ancomsd	⊢ ( ∃! 𝑥 𝜑 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
6	5	expdimp	⊢ ( ( ∃! 𝑥 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜑 → 𝑥 = 𝑦 ) )
7		pm13.13b	⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ 𝑥 = 𝑦 ) → 𝜑 )
8	7	ex	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( 𝑥 = 𝑦 → 𝜑 ) )
9	8	adantl	⊢ ( ( ∃! 𝑥 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
10	6 9	impbid	⊢ ( ( ∃! 𝑥 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → ( 𝜑 ↔ 𝑥 = 𝑦 ) )
11	10	ex	⊢ ( ∃! 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 → ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
12	1 2 11	alrimd	⊢ ( ∃! 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
13		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
14	13	eqcomd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → 𝑦 = ( ℩ 𝑥 𝜑 ) )
15	12 14	syl6	⊢ ( ∃! 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 = ( ℩ 𝑥 𝜑 ) ) )
16		iota4	⊢ ( ∃! 𝑥 𝜑 → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 )
17		dfsbcq	⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 ) )
18	16 17	syl5ibrcom	⊢ ( ∃! 𝑥 𝜑 → ( 𝑦 = ( ℩ 𝑥 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 ) )
19	15 18	impbid	⊢ ( ∃! 𝑥 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = ( ℩ 𝑥 𝜑 ) ) )
20	19	alrimiv	⊢ ( ∃! 𝑥 𝜑 → ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = ( ℩ 𝑥 𝜑 ) ) )