Theorem funopabeq

Description: A class of ordered pairs of values is a function. (Contributed by NM, 14-Nov-1995)

	Ref	Expression
Assertion	funopabeq	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		funopab	⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 } ↔ ∀ 𝑥 ∃* 𝑦 𝑦 = 𝐴 )
2		moeq	⊢ ∃* 𝑦 𝑦 = 𝐴
3	1 2	mpgbir	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = 𝐴 }