Metamath Proof Explorer


Theorem kqfval

Description: Value of the function appearing in df-kq . (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
Assertion kqfval ( ( 𝐽𝑉𝐴𝑋 ) → ( 𝐹𝐴 ) = { 𝑦𝐽𝐴𝑦 } )

Proof

Step Hyp Ref Expression
1 kqval.2 𝐹 = ( 𝑥𝑋 ↦ { 𝑦𝐽𝑥𝑦 } )
2 id ( 𝐴𝑋𝐴𝑋 )
3 rabexg ( 𝐽𝑉 → { 𝑦𝐽𝐴𝑦 } ∈ V )
4 eleq1 ( 𝑥 = 𝐴 → ( 𝑥𝑦𝐴𝑦 ) )
5 4 rabbidv ( 𝑥 = 𝐴 → { 𝑦𝐽𝑥𝑦 } = { 𝑦𝐽𝐴𝑦 } )
6 5 1 fvmptg ( ( 𝐴𝑋 ∧ { 𝑦𝐽𝐴𝑦 } ∈ V ) → ( 𝐹𝐴 ) = { 𝑦𝐽𝐴𝑦 } )
7 2 3 6 syl2anr ( ( 𝐽𝑉𝐴𝑋 ) → ( 𝐹𝐴 ) = { 𝑦𝐽𝐴𝑦 } )