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 | ⊢ ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ → ( 〈 𝐴 , 𝐵 〉 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 〈 𝐴 , 𝐵 〉 } ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov | ⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) | |
2 | 1 | neeq1i | ⊢ ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ ↔ ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) ≠ ∅ ) |
3 | fvfundmfvn0 | ⊢ ( ( 𝐹 ‘ 〈 𝐴 , 𝐵 〉 ) ≠ ∅ → ( 〈 𝐴 , 𝐵 〉 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 〈 𝐴 , 𝐵 〉 } ) ) ) | |
4 | 2 3 | sylbi | ⊢ ( ( 𝐴 𝐹 𝐵 ) ≠ ∅ → ( 〈 𝐴 , 𝐵 〉 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 〈 𝐴 , 𝐵 〉 } ) ) ) |