Theorem riota2f

Description: This theorem shows a condition that allows to represent a descriptor with a class expression B . (Contributed by NM, 23-Aug-2011) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	riota2f.1	⊢ Ⅎ 𝑥 𝐵
	riota2f.2	⊢ Ⅎ 𝑥 𝜓
	riota2f.3	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion	riota2f	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		riota2f.1	⊢ Ⅎ 𝑥 𝐵
2		riota2f.2	⊢ Ⅎ 𝑥 𝜓
3		riota2f.3	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
4	1	nfel1	⊢ Ⅎ 𝑥 𝐵 ∈ 𝐴
5	1	a1i	⊢ ( 𝐵 ∈ 𝐴 → Ⅎ 𝑥 𝐵 )
6	2	a1i	⊢ ( 𝐵 ∈ 𝐴 → Ⅎ 𝑥 𝜓 )
7		id	⊢ ( 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴 )
8	3	adantl	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝑥 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
9	4 5 6 7 8	riota2df	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )