This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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