Metamath Proof Explorer


Theorem riotacl2

Description: Membership law for "the unique element in A such that ph ". (Contributed by NM, 21-Aug-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Assertion riotacl2 ( ∃! 𝑥𝐴 𝜑 → ( 𝑥𝐴 𝜑 ) ∈ { 𝑥𝐴𝜑 } )

Proof

Step Hyp Ref Expression
1 df-reu ( ∃! 𝑥𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥𝐴𝜑 ) )
2 iotacl ( ∃! 𝑥 ( 𝑥𝐴𝜑 ) → ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) ) ∈ { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
3 1 2 sylbi ( ∃! 𝑥𝐴 𝜑 → ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) ) ∈ { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } )
4 df-riota ( 𝑥𝐴 𝜑 ) = ( ℩ 𝑥 ( 𝑥𝐴𝜑 ) )
5 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
6 3 4 5 3eltr4g ( ∃! 𝑥𝐴 𝜑 → ( 𝑥𝐴 𝜑 ) ∈ { 𝑥𝐴𝜑 } )