Theorem iota5f

Description: A method for computing iota. (Contributed by Scott Fenton, 13-Dec-2017)

	Ref	Expression
Hypotheses	iota5f.1	⊢ Ⅎ 𝑥 𝜑
	iota5f.2	⊢ Ⅎ 𝑥 𝐴
	iota5f.3	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
Assertion	iota5f	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		iota5f.1	⊢ Ⅎ 𝑥 𝜑
2		iota5f.2	⊢ Ⅎ 𝑥 𝐴
3		iota5f.3	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( 𝜓 ↔ 𝑥 = 𝐴 ) )
4	2	nfel1	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑉
5	1 4	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝐴 ∈ 𝑉 )
6	5 3	alrimi	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) )
7	2	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
8		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
9	8	bibi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
10	7 9	albid	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) ) )
11		eqeq2	⊢ ( 𝑦 = 𝐴 → ( ( ℩ 𝑥 𝜓 ) = 𝑦 ↔ ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
12	10 11	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) ) )
13		iotaval	⊢ ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝑦 ) → ( ℩ 𝑥 𝜓 ) = 𝑦 )
14	12 13	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ( 𝜓 ↔ 𝑥 = 𝐴 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 ) )
16	6 15	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → ( ℩ 𝑥 𝜓 ) = 𝐴 )