Theorem iota5

Description: A method for computing iota. (Contributed by NM, 17-Sep-2013)

	Ref	Expression
Hypothesis	iota5.1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
Assertion	iota5	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iota5.1	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
2	1	alrimiv	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) )
3		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
4	3	bibi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
5	4	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
6		eqeq2	⊢ ( 𝑦 = 𝐴 → ( ( ℩ 𝑥 𝜓 ) = 𝑦 ↔ ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
7	5 6	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) ) )
8		iotaval	⊢ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 )
9	7 8	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
11	2 10	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )