Theorem riotaprop

Description: Properties of a restricted definite description operator. (Contributed by NM, 23-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		riotaprop.0	⊢ Ⅎ 𝑥 𝜓
2		riotaprop.1	⊢ 𝐵 = ( ℩ 𝑥 ∈ 𝐴 𝜑 )
3		riotaprop.2	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
4		riotacl	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ 𝐴 )
5	2 4	eqeltrid	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → 𝐵 ∈ 𝐴 )
6	2	eqcomi	⊢ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵
7		nfriota1	⊢ Ⅎ 𝑥 ( ℩ 𝑥 ∈ 𝐴 𝜑 )
8	2 7	nfcxfr	⊢ Ⅎ 𝑥 𝐵
9	8 1 3	riota2f	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝜓 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) = 𝐵 ) )
10	6 9	mpbiri	⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → 𝜓 )
11	5 10	mpancom	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → 𝜓 )
12	5 11	jca	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( 𝐵 ∈ 𝐴 ∧ 𝜓 ) )