Theorem sbaniota

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

	Ref	Expression
Assertion	sbaniota	⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		eupickbi	⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
2		sbiota1	⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜓 ) ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )
3	1 2	bitrd	⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ [ ( ℩ 𝑥 𝜑 ) / 𝑥 ] 𝜓 ) )