This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∃! 𝑥 𝜑 → ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 = ( ℩ 𝑥 𝜑 ) ) )