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