Theorem riotasbc

Description: Substitution law for descriptions. Compare iotasbc . (Contributed by NM, 23-Aug-2011) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Assertion	riotasbc	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rabssab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∣ 𝜑 }
2		riotacl2	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝜑 } )
3	1 2	sselid	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ { 𝑥 ∣ 𝜑 } )
4		df-sbc	⊢ ( [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 ↔ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) ∈ { 𝑥 ∣ 𝜑 } )
5	3 4	sylibr	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → [ ( ℩ 𝑥 ∈ 𝐴 𝜑 ) / 𝑥 ] 𝜑 )