Description: If a class operation value for two operands is not the empty set, then the operands are contained in the domain of the class, and the class restricted to the operands is a function, analogous to fvfundmfvn0 . (Contributed by AV, 27-Jan-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | ovn0dmfun | |- ( ( A F B ) =/= (/) -> ( <. A , B >. e. dom F /\ Fun ( F |` { <. A , B >. } ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov | |- ( A F B ) = ( F ` <. A , B >. ) |
|
2 | 1 | neeq1i | |- ( ( A F B ) =/= (/) <-> ( F ` <. A , B >. ) =/= (/) ) |
3 | fvfundmfvn0 | |- ( ( F ` <. A , B >. ) =/= (/) -> ( <. A , B >. e. dom F /\ Fun ( F |` { <. A , B >. } ) ) ) |
|
4 | 2 3 | sylbi | |- ( ( A F B ) =/= (/) -> ( <. A , B >. e. dom F /\ Fun ( F |` { <. A , B >. } ) ) ) |