Metamath Proof Explorer

Theorem aovov0bi

Description: The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion aovov0bi 
|- ( ( A F B ) = (/) <-> ( (( A F B )) = (/) \/ (( A F B )) = _V ) )

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
2 1 eqeq1i 
 |-  ( ( A F B ) = (/) <-> ( F ` <. A , B >. ) = (/) )
3 afvfv0bi 
 |-  ( ( F ` <. A , B >. ) = (/) <-> ( ( F ''' <. A , B >. ) = (/) \/ ( F ''' <. A , B >. ) = _V ) )
4 df-aov 
 |-  (( A F B )) = ( F ''' <. A , B >. )
5 4 eqeq1i 
 |-  ( (( A F B )) = (/) <-> ( F ''' <. A , B >. ) = (/) )
6 5 bicomi 
 |-  ( ( F ''' <. A , B >. ) = (/) <-> (( A F B )) = (/) )
7 4 eqeq1i 
 |-  ( (( A F B )) = _V <-> ( F ''' <. A , B >. ) = _V )
8 7 bicomi 
 |-  ( ( F ''' <. A , B >. ) = _V <-> (( A F B )) = _V )
9 6 8 orbi12i 
 |-  ( ( ( F ''' <. A , B >. ) = (/) \/ ( F ''' <. A , B >. ) = _V ) <-> ( (( A F B )) = (/) \/ (( A F B )) = _V ) )
10 2 3 9 3bitri 
 |-  ( ( A F B ) = (/) <-> ( (( A F B )) = (/) \/ (( A F B )) = _V ) )