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	⊢ ( ¬ 𝐵 ∈ 𝐴 → ( 𝐹 ‘ 𝐵 ) = ∅ )