Theorem mptsuppdifd

Description: The support of a function in maps-to notation with a class difference. (Contributed by AV, 28-May-2019)

	Ref	Expression
Hypotheses	mptsuppdifd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	mptsuppdifd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	mptsuppdifd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
Assertion	mptsuppdifd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } )

Proof

Step	Hyp	Ref	Expression
1		mptsuppdifd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		mptsuppdifd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		mptsuppdifd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4	2	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
5	1 4	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ V )
6		suppimacnv	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7	5 3 6	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
8	1	mptpreima	⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) }
9	7 8	eqtrdi	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } )