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 F = x A B
mptsuppdifd.a φ A V
mptsuppdifd.z φ Z W
Assertion mptsuppdifd φ F supp Z = x A | B V Z

Proof

Step Hyp Ref Expression
1 mptsuppdifd.f F = x A B
2 mptsuppdifd.a φ A V
3 mptsuppdifd.z φ Z W
4 2 mptexd φ x A B V
5 1 4 eqeltrid φ F V
6 suppimacnv F V Z W F supp Z = F -1 V Z
7 5 3 6 syl2anc φ F supp Z = F -1 V Z
8 1 mptpreima F -1 V Z = x A | B V Z
9 7 8 eqtrdi φ F supp Z = x A | B V Z