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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
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 𝑍 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝑍 } )