Description: Value of the function appearing in df-kq . (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | kqval.2 | ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) | |
Assertion | kqfval | ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } ) |
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 | ⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } ) |