Theorem aovvdm

Description: If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	aovvdm	⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
2	1	eleq1i	⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 ↔ ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝐶 )
3		afvvdm	⊢ ( ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) ∈ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
4	2 3	sylbi	⊢ ( (( 𝐴 𝐹 𝐵 )) ∈ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )