Metamath Proof Explorer


Theorem fvopab4ndm

Description: Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008)

Ref Expression
Hypothesis fvopab4ndm.1 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜑 ) }
Assertion fvopab4ndm ( ¬ 𝐵𝐴 → ( 𝐹𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 fvopab4ndm.1 𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜑 ) }
2 1 dmeqi dom 𝐹 = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜑 ) }
3 dmopabss dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝜑 ) } ⊆ 𝐴
4 2 3 eqsstri dom 𝐹𝐴
5 4 sseli ( 𝐵 ∈ dom 𝐹𝐵𝐴 )
6 ndmfv ( ¬ 𝐵 ∈ dom 𝐹 → ( 𝐹𝐵 ) = ∅ )
7 5 6 nsyl5 ( ¬ 𝐵𝐴 → ( 𝐹𝐵 ) = ∅ )