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 ) |
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 ) |