Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 mptsuppdifd.f F = x A B
2 mptsuppdifd.a φ A V
3 mptsuppdifd.z φ Z W
4 mptsuppd.b φ x A B U
5 1 2 3 mptsuppdifd φ F supp Z = x A | B V Z
6 eldifsn B V Z B V B Z
7 4 elexd φ x A B V
8 7 biantrurd φ x A B Z B V B Z
9 6 8 bitr4id φ x A B V Z B Z
10 9 rabbidva φ x A | B V Z = x A | B Z
11 5 10 eqtrd φ F supp Z = x A | B Z