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

Metamath Proof Explorer

Theorem iotasbc

Description: Definition *14.01 in WhiteheadRussell p. 184. In Principia Mathematica, Russell and Whitehead define iota in terms of a function of ( iota x ph ) . Their definition differs in that a function of ( iota x ph ) evaluates to "false" when there isn't a single x that satisfies ph . (Contributed by Andrew Salmon, 11-Jul-2011)

Ref Expression
Assertion iotasbc ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 sbc5 ⊢ ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) )
2 iotaexeu ⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
3 eueq ⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V ↔ ∃! 𝑦 𝑦 = ( ℩ 𝑥 𝜑 ) )
4 2 3 sylib ⊢ ( ∃! 𝑥 𝜑 → ∃! 𝑦 𝑦 = ( ℩ 𝑥 𝜑 ) )
5 eu6 ⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
6 iotaval ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
7 6 eqcomd ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → 𝑦 = ( ℩ 𝑥 𝜑 ) )
8 7 ancri ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
9 8 eximi ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
10 5 9 sylbi ⊢ ( ∃! 𝑥 𝜑 → ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
11 eupick ⊢ ( ( ∃! 𝑦 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) ) → ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
12 4 10 11 syl2anc ⊢ ( ∃! 𝑥 𝜑 → ( 𝑦 = ( ℩ 𝑥 𝜑 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
13 12 7 impbid1 ⊢ ( ∃! 𝑥 𝜑 → ( 𝑦 = ( ℩ 𝑥 𝜑 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
14 13 anbi1d ⊢ ( ∃! 𝑥 𝜑 → ( ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝜓 ) ) )
15 14 exbidv ⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑦 ( 𝑦 = ( ℩ 𝑥 𝜑 ) ∧ 𝜓 ) ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝜓 ) ) )
16 1 15 bitrid ⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑦 ] 𝜓 ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝜓 ) ) )