Metamath Proof Explorer


Theorem aov0ov0

Description: If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion aov0ov0
|- ( (( A F B )) = (/) -> ( A F B ) = (/) )

Proof

Step Hyp Ref Expression
1 afv0fv0
 |-  ( ( F ''' <. A , B >. ) = (/) -> ( F ` <. A , B >. ) = (/) )
2 df-aov
 |-  (( A F B )) = ( F ''' <. A , B >. )
3 2 eqeq1i
 |-  ( (( A F B )) = (/) <-> ( F ''' <. A , B >. ) = (/) )
4 df-ov
 |-  ( A F B ) = ( F ` <. A , B >. )
5 4 eqeq1i
 |-  ( ( A F B ) = (/) <-> ( F ` <. A , B >. ) = (/) )
6 1 3 5 3imtr4i
 |-  ( (( A F B )) = (/) -> ( A F B ) = (/) )