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	⊢ ( ( 𝐽 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) = { 𝑦 ∈ 𝐽 ∣ 𝐴 ∈ 𝑦 } )