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

Metamath Proof Explorer

Theorem sbiota1

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

Ref Expression
Assertion sbiota1 ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 eu6 ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
2 1 biimpi ⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
3 iota4 ⊢ ( ∃! 𝑥 𝜑 → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 )
4 iotaval ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
5 4 eqcomd ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → 𝑦 = ( ℩ 𝑥 𝜑 ) )
6 spsbim ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
7 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
8 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝑦 / 𝑥 ] 𝜓 )
9 6 7 8 3imtr3g ⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
10 dfsbcq ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 ) )
11 dfsbcq ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )
12 10 11 imbi12d ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
13 9 12 imbitrid ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
14 13 com23 ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
15 5 14 syl ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
16 15 exlimiv ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
17 2 3 16 sylc ⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )
18 iotaexeu ⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
19 10 11 anbi12d ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 ∧ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) ) )
20 19 imbi1d ⊢ ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ( ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 ∧ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) )
21 sbcan ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
22 spesbc ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
23 21 22 sylbir ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
24 20 23 vtoclg ⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V → ( ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 ∧ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
25 24 expd ⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) )
26 18 3 25 sylc ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 → ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) )
27 26 anc2li ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 → ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) ) )
28 eupicka ⊢ ( ( ∃! 𝑥 𝜑 ∧ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
29 27 28 syl6 ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
30 17 29 impbid ⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )