Metamath Proof Explorer


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
|- ( (( A F B )) e. C -> <. A , B >. e. dom F )

Proof

Step Hyp Ref Expression
1 df-aov
 |-  (( A F B )) = ( F ''' <. A , B >. )
2 1 eleq1i
 |-  ( (( A F B )) e. C <-> ( F ''' <. A , B >. ) e. C )
3 afvvdm
 |-  ( ( F ''' <. A , B >. ) e. C -> <. A , B >. e. dom F )
4 2 3 sylbi
 |-  ( (( A F B )) e. C -> <. A , B >. e. dom F )