Theorem mptsuppd

Description: The support of a function in maps-to notation. (Contributed by AV, 10-Apr-2019) (Revised by AV, 28-May-2019)

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

Proof

Step	Hyp	Ref	Expression
1		mptsuppdifd.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		mptsuppdifd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		mptsuppdifd.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑊 )
4		mptsuppd.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑈 )
5	1 2 3	mptsuppdifd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } )
6		eldifsn	⊢ ( 𝐵 ∈ ( V ∖ { 𝑍 } ) ↔ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝑍 ) )
7	4	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V )
8	7	biantrurd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≠ 𝑍 ↔ ( 𝐵 ∈ V ∧ 𝐵 ≠ 𝑍 ) ) )
9	6 8	bitr4id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ∈ ( V ∖ { 𝑍 } ) ↔ 𝐵 ≠ 𝑍 ) )
10	9	rabbidva	⊢ ( 𝜑 → { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ ( V ∖ { 𝑍 } ) } = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍 } )
11	5 10	eqtrd	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍 } )