Theorem iotavalb

Description: Theorem *14.202 in WhiteheadRussell p. 189. A biconditional version of iotaval . (Contributed by Andrew Salmon, 11-Jul-2011)

	Ref	Expression
Assertion	iotavalb	⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		iotaval	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜑 ) = 𝑦 )
2		iotasbc	⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) ) )
3		iotaexeu	⊢ ( ∃! 𝑥 𝜑 → ( ℩ 𝑥 𝜑 ) ∈ V )
4		eqsbc1	⊢ ( ( ℩ 𝑥 𝜑 ) ∈ V → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
5	3 4	syl	⊢ ( ∃! 𝑥 𝜑 → ( [ ( ℩ 𝑥 𝜑 ) / 𝑧 ] 𝑧 = 𝑦 ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
6	2 5	bitr3d	⊢ ( ∃! 𝑥 𝜑 → ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )
7		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
8	7	bibi2d	⊢ ( 𝑧 = 𝑦 → ( ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
9	8	albidv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
10	9	biimpac	⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
11	10	exlimiv	⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑧 ) ∧ 𝑧 = 𝑦 ) → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
12	6 11	syl6bir	⊢ ( ∃! 𝑥 𝜑 → ( ( ℩ 𝑥 𝜑 ) = 𝑦 → ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ) )
13	1 12	impbid2	⊢ ( ∃! 𝑥 𝜑 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ℩ 𝑥 𝜑 ) = 𝑦 ) )