Theorem funopab4

Description: A class of ordered pairs of values in the form used by df-mpt is a function. (Contributed by NM, 17-Feb-2013)

	Ref	Expression
Assertion	funopab4	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐴 ) }

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝜑 ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
2	1	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐴 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 }
3		funopabeq	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 }
4		funss	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐴 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 } → ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 } → Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐴 ) } ) )
5	2 3 4	mp2	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∧ 𝑦 = 𝐴 ) }