Metamath Proof Explorer


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 ∖ { 𝑍 } ) } )