Metamath Proof Explorer


Theorem riotasv

Description: Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ). Special case of riota2f . (Contributed by NM, 26-Jan-2013) (Proof shortened by Mario Carneiro, 6-Dec-2016)

Ref Expression
Hypotheses riotasv.1 𝐴 ∈ V
riotasv.2 𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝐶 ) )
Assertion riotasv ( ( 𝐷𝐴𝑦𝐵𝜑 ) → 𝐷 = 𝐶 )

Proof

Step Hyp Ref Expression
1 riotasv.1 𝐴 ∈ V
2 riotasv.2 𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝐶 ) )
3 2 a1i ( 𝐷𝐴𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜑𝑥 = 𝐶 ) ) )
4 id ( 𝐷𝐴𝐷𝐴 )
5 3 4 riotasvd ( ( 𝐷𝐴𝐴 ∈ V ) → ( ( 𝑦𝐵𝜑 ) → 𝐷 = 𝐶 ) )
6 1 5 mpan2 ( 𝐷𝐴 → ( ( 𝑦𝐵𝜑 ) → 𝐷 = 𝐶 ) )
7 6 3impib ( ( 𝐷𝐴𝑦𝐵𝜑 ) → 𝐷 = 𝐶 )