Metamath Proof Explorer


Theorem ovn0ssdmfun

Description: If a class' operation value for two operands is not the empty set, 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 ovn0ssdmfun a D b E a F b D × E dom F Fun F D × E

Proof

Step Hyp Ref Expression
1 fveq2 p = a b F p = F a b
2 df-ov a F b = F a b
3 1 2 eqtr4di p = a b F p = a F b
4 3 neeq1d p = a b F p a F b
5 4 ralxp p D × E F p a D b E a F b
6 fvn0ssdmfun p D × E F p D × E dom F Fun F D × E
7 5 6 sylbir a D b E a F b D × E dom F Fun F D × E